Sundstrom page243_proposition5.10

hughmcguire

Proof of the following formula: 

A = B ∪ {x}
  →
(∀S)
  (S ⊆ A  →  S ⊆ B  ∨  (∃C)[S = C ∪ {x}  ∧  C ⊆ B])

(#) Comments Suppositions and derivations Theorem and subgoals
    We presuppose the following:  
(1)   
(∀u,S)[u ∉ S  ∨  u ∈ S]
 
(2)   
(∀S1,S2)(S1 ⊆ S2  means  (∀u)[if u ∈ S1, then u ∈ S2])
 
(3)   
(∀u,S1,S2)[u ∈ S1 ∪ S2  means  u ∈ S1  or  u ∈ S2]
 
(4)   
(∀u,v)[u ∈ {v}  ↔  u = v]
 
(5)   
(∀u,S)[u ∈ S  ↔  {u} ⊆ S]
 
(6)   
(∀S1,S2,S3)[S1 ⊆ S2  →  (S2 ⊆ S3 ∪ S1  ↔  S2 - S1 ⊆ S3)]
 
(7)   
(∀S1,S2)[S1 ⊆ S2  ↔  S2 = S2 ∪ S1]
 
(8)   
(∀S1,S2)[(S1 - S2) ∪ S2 = S1 ∪ S2]
 
       
      We start working with the formula being proved
as follows:
(9)     
A = B ∪ {x}
  →
(∀S)
  (S ⊆ A  →  S ⊆ B  ∨  (∃C)[S = C ∪ {x}  ∧  C ⊆ B])
    We'll assume that formula's antecedent:  
(10)   
A = B ∪ {x}
 
      and we'll work on proving the consequent:
(11)     
(∀S)
  (S ⊆ A  →  S ⊆ B  ∨  (∃C)[S = C ∪ {x}  ∧  C ⊆ B])
      Well, let an arbitrary value "Y" be given;
then we should prove the following:
(12)     
Y ⊆ A  →  Y ⊆ B  ∨  (∃C)[Y = C ∪ {x}  ∧  C ⊆ B]
    We'll assume that formula's antecedent:  
(13)   
Y ⊆ A
 
      and we'll work on proving a consequent:
(14)     
Y ⊆ B
      or alternatively:
(15)     
(∃C)[Y = C ∪ {x}  ∧  C ⊆ B]
      Assigning "C := Y-{x}" in that formula yields:
(16)     
Y = (Y - {x}) ∪ {x}  ∧  (Y - {x}) ⊆ B
    Applying the equation in formula (10)
to the selection in formula (13)
yields: 		 
(17)   
Y ⊆ (B ∪ {x})
 
        ≡      by (2) with "S1 := Y, S2 := B∪{x}"  
(18)   
(∀u)[if u ∈ Y,  then  u ∈ (B ∪ {x})]
 
        ≡      by (3) with "u := u, S1 := B, S2 := {x}"  
(19)   
(∀u)[if u ∈ Y, then (u ∈ B  or  u ∈ {x})]
 
        ≡      by (4) with "u := u, v := x"  
(20)   
(∀u)[if u ∈ Y, then (u ∈ B  or  [u = x])]
 
    Assigning "u,S := x,Y" in formula (1) yields:  
(21)   
x ∉ Y  ∨  x ∈ Y
 
      Applying the equivalence in formula (2)
to formula (14)
with "S1 := Y, S2 := B"
yields:
(22)     
(∀u)[if u ∈ Y,  then  u ∈ B]
      Well, let an arbitrary value "y" be given;
then we should prove the following:
(23)     
if y ∈ Y,  then  y ∈ B
    We'll assume that formula's antecedent:  
(24)   
y ∈ Y
 
      and we'll work on proving the consequent:
(25)     
y ∈ B
    Applying formula (20) to formula (24)
with "u := y"
yields: 		 
(26)   
y ∈ B  or  [y = x]
 
       
    We'll handle formula (21)'s components
in separate subparts of this proof, as follows: 		 
    Case 1:  
(27)   
x ∉ Y
 
        ≡      by (26)  
(28)   
(y ∈ B) ∨ [y ∉ Y]
 
        ≡      by rewriting the form "τ1 ∉ τ2"
        to "¬(τ1 ∈ τ2)" 		 
(29)   
(y ∈ B) ∨ [¬(y ∈ Y)]
 
        ↓      by (24)  
(30)   
y ∈ B
 
      And formula (30) matches formula (25)
so we get:
(31)     
true
      That concludes this part of the proof.
       
    Case 2:  
(32)   
x ∈ Y
 
        ≡      by (5) with "u := x, S := Y"  
(33)   
{x} ⊆ Y
 
        ↓      by (6) with "S1 := {x}, S2 := Y"  
(34)   
Y  ⊆  S3 ∪ {x}  ↔  Y - {x}  ⊆  S3
 
    Applying that equivalence to formula (17)
with "S3 := B"
yields: 		 
(35)   
Y - {x}  ⊆  B
 
          ↓      by (16)
(36)     
Y = (Y - {x}) ∪ {x}  ∧  true
          ≡      by simplifying
(37)     
Y = (Y - {x}) ∪ {x}
    Applying the equivalence in formula (7)
to formula (33)
with "S1 := {x}, S2 := Y"
yields: 		 
(38)   
Y = Y ∪ {x}
 
        ≡      by (8) with "S1 := Y, S2 := {x}"  
(39)   
Y = [(Y - {x}) ∪ {x}]
 
      And formula (39) matches formula (37)
so we get:
(40)     
true
      That concludes this part of the proof.
       
      Thus, the theorem that was given is true,
by the above partitioning of this proof into subparts.

identification:
1216840805215
1216840027692
777523