dfaddc2 - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > dfaddc2		GIF version

Theorem dfaddc2 4382

Description: Alternate definition of cardinal addition to establish stratification. (Contributed by SF, 15-Jan-2015.)

**Assertion**
Ref	Expression
dfaddc2	⊢ (A +_c B) = ((( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁B) “_k A)

Proof of Theorem dfaddc2 Dummy variables x y z t w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-addc 4379	. 2 ⊢ (A +_c B) = {x ∣ ∃y ∈ A ∃z ∈ B ((y ∩ z) = ∅ ∧ x = (y ∪ z))}
2		vex 2863	. . . . 5 ⊢ x ∈ V
3	2	elimak 4260	. . . 4 ⊢ (x ∈ ((( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁B) “_k A) ↔ ∃y ∈ A ⟪y, x⟫ ∈ (( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁B))
4		opkex 4114	. . . . . . 7 ⊢ ⟪y, x⟫ ∈ V
5	4	elimak 4260	. . . . . 6 ⊢ (⟪y, x⟫ ∈ (( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁B) ↔ ∃t ∈ ℘₁ ℘₁B⟪t, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)))
6		elpw12 4146	. . . . . . . . . 10 ⊢ (t ∈ ℘₁℘₁B ↔ ∃z ∈ B t = {{z}})
7	6	anbi1i 676	. . . . . . . . 9 ⊢ ((t ∈ ℘₁℘₁B ∧ ⟪t, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c))) ↔ (∃z ∈ B t = {{z}} ∧ ⟪t, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c))))
8		r19.41v 2765	. . . . . . . . 9 ⊢ (∃z ∈ B (t = {{z}} ∧ ⟪t, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c))) ↔ (∃z ∈ B t = {{z}} ∧ ⟪t, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c))))
9	7, 8	bitr4i 243	. . . . . . . 8 ⊢ ((t ∈ ℘₁℘₁B ∧ ⟪t, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c))) ↔ ∃z ∈ B (t = {{z}} ∧ ⟪t, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c))))
10	9	exbii 1582	. . . . . . 7 ⊢ (∃t(t ∈ ℘₁℘₁B ∧ ⟪t, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c))) ↔ ∃t∃z ∈ B (t = {{z}} ∧ ⟪t, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c))))
11		df-rex 2621	. . . . . . 7 ⊢ (∃t ∈ ℘₁ ℘₁B⟪t, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) ↔ ∃t(t ∈ ℘₁℘₁B ∧ ⟪t, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c))))
12		rexcom4 2879	. . . . . . 7 ⊢ (∃z ∈ B ∃t(t = {{z}} ∧ ⟪t, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c))) ↔ ∃t∃z ∈ B (t = {{z}} ∧ ⟪t, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c))))
13	10, 11, 12	3bitr4i 268	. . . . . 6 ⊢ (∃t ∈ ℘₁ ℘₁B⟪t, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) ↔ ∃z ∈ B ∃t(t = {{z}} ∧ ⟪t, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c))))
14		snex 4112	. . . . . . . . 9 ⊢ {{z}} ∈ V
15		opkeq1 4060	. . . . . . . . . 10 ⊢ (t = {{z}} → ⟪t, ⟪y, x⟫⟫ = ⟪{{z}}, ⟪y, x⟫⟫)
16	15	eleq1d 2419	. . . . . . . . 9 ⊢ (t = {{z}} → (⟪t, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) ↔ ⟪{{z}}, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c))))
17	14, 16	ceqsexv 2895	. . . . . . . 8 ⊢ (∃t(t = {{z}} ∧ ⟪t, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c))) ↔ ⟪{{z}}, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)))
18		eldif 3222	. . . . . . . 8 ⊢ (⟪{{z}}, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) ↔ (⟪{{z}}, ⟪y, x⟫⟫ ∈ Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∧ ¬ ⟪{{z}}, ⟪y, x⟫⟫ ∈ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)))
19		opkex 4114	. . . . . . . . . . . 12 ⊢ ⟪z, y⟫ ∈ V
20	19	elcompl 3226	. . . . . . . . . . 11 ⊢ (⟪z, y⟫ ∈ ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ¬ ⟪z, y⟫ ∈ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))
21		vex 2863	. . . . . . . . . . . . 13 ⊢ z ∈ V
22		vex 2863	. . . . . . . . . . . . 13 ⊢ y ∈ V
23	21, 22	ndisjrelk 4324	. . . . . . . . . . . 12 ⊢ (⟪z, y⟫ ∈ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ (z ∩ y) ≠ ∅)
24	23	necon2bbii 2573	. . . . . . . . . . 11 ⊢ ((z ∩ y) = ∅ ↔ ¬ ⟪z, y⟫ ∈ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))
25	20, 24	bitr4i 243	. . . . . . . . . 10 ⊢ (⟪z, y⟫ ∈ ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ (z ∩ y) = ∅)
26	21, 22, 2	otkelins3k 4257	. . . . . . . . . 10 ⊢ (⟪{{z}}, ⟪y, x⟫⟫ ∈ Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ ⟪z, y⟫ ∈ ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c))
27		incom 3449	. . . . . . . . . . 11 ⊢ (y ∩ z) = (z ∩ y)
28	27	eqeq1i 2360	. . . . . . . . . 10 ⊢ ((y ∩ z) = ∅ ↔ (z ∩ y) = ∅)
29	25, 26, 28	3bitr4i 268	. . . . . . . . 9 ⊢ (⟪{{z}}, ⟪y, x⟫⟫ ∈ Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ (y ∩ z) = ∅)
30		dfcleq 2347	. . . . . . . . . 10 ⊢ (x = (y ∪ z) ↔ ∀w(w ∈ x ↔ w ∈ (y ∪ z)))
31		opkex 4114	. . . . . . . . . . . . . 14 ⊢ ⟪{{z}}, ⟪y, x⟫⟫ ∈ V
32	31	elimak 4260	. . . . . . . . . . . . 13 ⊢ (⟪{{z}}, ⟪y, x⟫⟫ ∈ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ↔ ∃t ∈ ℘₁ ℘₁℘₁℘₁1_c⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )))
33		df-rex 2621	. . . . . . . . . . . . 13 ⊢ (∃t ∈ ℘₁ ℘₁℘₁℘₁1_c⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) ↔ ∃t(t ∈ ℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k ))))
34		elpw141c 4151	. . . . . . . . . . . . . . . . 17 ⊢ (t ∈ ℘₁℘₁℘₁℘₁1_c ↔ ∃w t = {{{{{w}}}}})
35	34	anbi1i 676	. . . . . . . . . . . . . . . 16 ⊢ ((t ∈ ℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k ))) ↔ (∃w t = {{{{{w}}}}} ∧ ⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k ))))
36		19.41v 1901	. . . . . . . . . . . . . . . 16 ⊢ (∃w(t = {{{{{w}}}}} ∧ ⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k ))) ↔ (∃w t = {{{{{w}}}}} ∧ ⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k ))))
37	35, 36	bitr4i 243	. . . . . . . . . . . . . . 15 ⊢ ((t ∈ ℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k ))) ↔ ∃w(t = {{{{{w}}}}} ∧ ⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k ))))
38	37	exbii 1582	. . . . . . . . . . . . . 14 ⊢ (∃t(t ∈ ℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k ))) ↔ ∃t∃w(t = {{{{{w}}}}} ∧ ⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k ))))
39		excom 1741	. . . . . . . . . . . . . 14 ⊢ (∃w∃t(t = {{{{{w}}}}} ∧ ⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k ))) ↔ ∃t∃w(t = {{{{{w}}}}} ∧ ⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k ))))
40	38, 39	bitr4i 243	. . . . . . . . . . . . 13 ⊢ (∃t(t ∈ ℘₁℘₁℘₁℘₁1_c ∧ ⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k ))) ↔ ∃w∃t(t = {{{{{w}}}}} ∧ ⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k ))))
41	32, 33, 40	3bitri 262	. . . . . . . . . . . 12 ⊢ (⟪{{z}}, ⟪y, x⟫⟫ ∈ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ↔ ∃w∃t(t = {{{{{w}}}}} ∧ ⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k ))))
42		snex 4112	. . . . . . . . . . . . . . 15 ⊢ {{{{{w}}}}} ∈ V
43		opkeq1 4060	. . . . . . . . . . . . . . . 16 ⊢ (t = {{{{{w}}}}} → ⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ = ⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫)
44	43	eleq1d 2419	. . . . . . . . . . . . . . 15 ⊢ (t = {{{{{w}}}}} → (⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) ↔ ⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k ))))
45	42, 44	ceqsexv 2895	. . . . . . . . . . . . . 14 ⊢ (∃t(t = {{{{{w}}}}} ∧ ⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k ))) ↔ ⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )))
46		elsymdif 3224	. . . . . . . . . . . . . 14 ⊢ (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) ↔ ¬ (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ Ins2_k Ins2_k S_k ↔ ⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )))
47		snex 4112	. . . . . . . . . . . . . . . . . 18 ⊢ {{{w}}} ∈ V
48	47, 14, 4	otkelins2k 4256	. . . . . . . . . . . . . . . . 17 ⊢ (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ Ins2_k Ins2_k S_k ↔ ⟪{{{w}}}, ⟪y, x⟫⟫ ∈ Ins2_k S_k )
49		snex 4112	. . . . . . . . . . . . . . . . . 18 ⊢ {w} ∈ V
50	49, 22, 2	otkelins2k 4256	. . . . . . . . . . . . . . . . 17 ⊢ (⟪{{{w}}}, ⟪y, x⟫⟫ ∈ Ins2_k S_k ↔ ⟪{w}, x⟫ ∈ S_k )
51		vex 2863	. . . . . . . . . . . . . . . . . 18 ⊢ w ∈ V
52	51, 2	elssetk 4271	. . . . . . . . . . . . . . . . 17 ⊢ (⟪{w}, x⟫ ∈ S_k ↔ w ∈ x)
53	48, 50, 52	3bitri 262	. . . . . . . . . . . . . . . 16 ⊢ (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ Ins2_k Ins2_k S_k ↔ w ∈ x)
54	47, 14, 4	otkelins2k 4256	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ Ins2_k Ins3_k S_k ↔ ⟪{{{w}}}, ⟪y, x⟫⟫ ∈ Ins3_k S_k )
55	49, 22, 2	otkelins3k 4257	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟪{{{w}}}, ⟪y, x⟫⟫ ∈ Ins3_k S_k ↔ ⟪{w}, y⟫ ∈ S_k )
56	51, 22	elssetk 4271	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟪{w}, y⟫ ∈ S_k ↔ w ∈ y)
57	54, 55, 56	3bitri 262	. . . . . . . . . . . . . . . . . 18 ⊢ (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ Ins2_k Ins3_k S_k ↔ w ∈ y)
58	47, 14, 4	otkelins3k 4257	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ Ins3_k SI_k SI_k S_k ↔ ⟪{{{w}}}, {{z}}⟫ ∈ SI_k SI_k S_k )
59		snex 4112	. . . . . . . . . . . . . . . . . . . 20 ⊢ {{w}} ∈ V
60		snex 4112	. . . . . . . . . . . . . . . . . . . 20 ⊢ {z} ∈ V
61	59, 60	opksnelsik 4266	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟪{{{w}}}, {{z}}⟫ ∈ SI_k SI_k S_k ↔ ⟪{{w}}, {z}⟫ ∈ SI_k S_k )
62	49, 21	opksnelsik 4266	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟪{{w}}, {z}⟫ ∈ SI_k S_k ↔ ⟪{w}, z⟫ ∈ S_k )
63	51, 21	elssetk 4271	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟪{w}, z⟫ ∈ S_k ↔ w ∈ z)
64	62, 63	bitri 240	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟪{{w}}, {z}⟫ ∈ SI_k S_k ↔ w ∈ z)
65	58, 61, 64	3bitri 262	. . . . . . . . . . . . . . . . . 18 ⊢ (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ Ins3_k SI_k SI_k S_k ↔ w ∈ z)
66	57, 65	orbi12i 507	. . . . . . . . . . . . . . . . 17 ⊢ ((⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ Ins2_k Ins3_k S_k ∨ ⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ Ins3_k SI_k SI_k S_k ) ↔ (w ∈ y ∨ w ∈ z))
67		elun 3221	. . . . . . . . . . . . . . . . 17 ⊢ (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k ) ↔ (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ Ins2_k Ins3_k S_k ∨ ⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ Ins3_k SI_k SI_k S_k ))
68		elun 3221	. . . . . . . . . . . . . . . . 17 ⊢ (w ∈ (y ∪ z) ↔ (w ∈ y ∨ w ∈ z))
69	66, 67, 68	3bitr4i 268	. . . . . . . . . . . . . . . 16 ⊢ (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k ) ↔ w ∈ (y ∪ z))
70	53, 69	bibi12i 306	. . . . . . . . . . . . . . 15 ⊢ ((⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ Ins2_k Ins2_k S_k ↔ ⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) ↔ (w ∈ x ↔ w ∈ (y ∪ z)))
71	70	notbii 287	. . . . . . . . . . . . . 14 ⊢ (¬ (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ Ins2_k Ins2_k S_k ↔ ⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) ↔ ¬ (w ∈ x ↔ w ∈ (y ∪ z)))
72	45, 46, 71	3bitri 262	. . . . . . . . . . . . 13 ⊢ (∃t(t = {{{{{w}}}}} ∧ ⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k ))) ↔ ¬ (w ∈ x ↔ w ∈ (y ∪ z)))
73	72	exbii 1582	. . . . . . . . . . . 12 ⊢ (∃w∃t(t = {{{{{w}}}}} ∧ ⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ ( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k ))) ↔ ∃w ¬ (w ∈ x ↔ w ∈ (y ∪ z)))
74		exnal 1574	. . . . . . . . . . . 12 ⊢ (∃w ¬ (w ∈ x ↔ w ∈ (y ∪ z)) ↔ ¬ ∀w(w ∈ x ↔ w ∈ (y ∪ z)))
75	41, 73, 74	3bitri 262	. . . . . . . . . . 11 ⊢ (⟪{{z}}, ⟪y, x⟫⟫ ∈ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ↔ ¬ ∀w(w ∈ x ↔ w ∈ (y ∪ z)))
76	75	con2bii 322	. . . . . . . . . 10 ⊢ (∀w(w ∈ x ↔ w ∈ (y ∪ z)) ↔ ¬ ⟪{{z}}, ⟪y, x⟫⟫ ∈ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c))
77	30, 76	bitr2i 241	. . . . . . . . 9 ⊢ (¬ ⟪{{z}}, ⟪y, x⟫⟫ ∈ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c) ↔ x = (y ∪ z))
78	29, 77	anbi12i 678	. . . . . . . 8 ⊢ ((⟪{{z}}, ⟪y, x⟫⟫ ∈ Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∧ ¬ ⟪{{z}}, ⟪y, x⟫⟫ ∈ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) ↔ ((y ∩ z) = ∅ ∧ x = (y ∪ z)))
79	17, 18, 78	3bitri 262	. . . . . . 7 ⊢ (∃t(t = {{z}} ∧ ⟪t, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c))) ↔ ((y ∩ z) = ∅ ∧ x = (y ∪ z)))
80	79	rexbii 2640	. . . . . 6 ⊢ (∃z ∈ B ∃t(t = {{z}} ∧ ⟪t, ⟪y, x⟫⟫ ∈ ( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c))) ↔ ∃z ∈ B ((y ∩ z) = ∅ ∧ x = (y ∪ z)))
81	5, 13, 80	3bitri 262	. . . . 5 ⊢ (⟪y, x⟫ ∈ (( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁B) ↔ ∃z ∈ B ((y ∩ z) = ∅ ∧ x = (y ∪ z)))
82	81	rexbii 2640	. . . 4 ⊢ (∃y ∈ A ⟪y, x⟫ ∈ (( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁B) ↔ ∃y ∈ A ∃z ∈ B ((y ∩ z) = ∅ ∧ x = (y ∪ z)))
83	3, 82	bitri 240	. . 3 ⊢ (x ∈ ((( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁B) “_k A) ↔ ∃y ∈ A ∃z ∈ B ((y ∩ z) = ∅ ∧ x = (y ∪ z)))
84	83	abbi2i 2465	. 2 ⊢ ((( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁B) “_k A) = {x ∣ ∃y ∈ A ∃z ∈ B ((y ∩ z) = ∅ ∧ x = (y ∪ z))}
85	1, 84	eqtr4i 2376	1 ⊢ (A +_c B) = ((( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k ℘₁℘₁℘₁℘₁1_c)) “_k ℘₁℘₁B) “_k A)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 176 ∨ wo 357 ∧ wa 358 ∀wal 1540 ∃wex 1541 = wceq 1642 ∈ wcel 1710 {cab 2339 ∃wrex 2616 ∼ ccompl 3206 ∖ cdif 3207 ∪ cun 3208 ∩ cin 3209 ⊕ csymdif 3210 ∅c0 3551 {csn 3738 ⟪copk 4058 1_cc1c 4135 ℘₁cpw1 4136 Ins2_k cins2k 4177 Ins3_k cins3k 4178 “_k cimak 4180 SI_k csik 4182 S_k cssetk 4184 +_c cplc 4376

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4079 ax-sn 4088

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2479 df-ne 2519 df-rex 2621 df-v 2862 df-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-symdif 3217 df-ss 3260 df-nul 3552 df-pw 3725 df-sn 3742 df-pr 3743 df-opk 4059 df-1c 4137 df-pw1 4138 df-ins2k 4188 df-ins3k 4189 df-imak 4190 df-sik 4193 df-ssetk 4194 df-addc 4379

This theorem is referenced by: addceq1 4384 addceq2 4385 addcexg 4394 dfnnc2 4396 nnc0suc 4413 nncaddccl 4420 nnsucelrlem1 4425 preaddccan2lem1 4455 ltfinex 4465 evenodddisjlem1 4516 dfphi2 4570 phialllem1 4617

W3C validator