dfaddc2 - New Foundations Explorer

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

Theorem dfaddc2 4381

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 4378	. 2 ⊢ (A +_c B) = {x ∣ ∃y ∈ A ∃z ∈ B ((y ∩ z) = ∅ ∧ x = (y ∪ z))}
2		vex 2862	. . . . 5 ⊢ x ∈ V
3	2	elimak 4259	. . . 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 4113	. . . . . . 7 ⊢ ⟪y, x⟫ ∈ V
5	4	elimak 4259	. . . . . 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 4145	. . . . . . . . . 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 2764	. . . . . . . . 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 2620	. . . . . . 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 2878	. . . . . . 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 4111	. . . . . . . . 9 ⊢ {{z}} ∈ V
15		opkeq1 4059	. . . . . . . . . 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 2894	. . . . . . . 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 3221	. . . . . . . 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 4113	. . . . . . . . . . . 12 ⊢ ⟪z, y⟫ ∈ V
20	19	elcompl 3225	. . . . . . . . . . 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 2862	. . . . . . . . . . . . 13 ⊢ z ∈ V
22		vex 2862	. . . . . . . . . . . . 13 ⊢ y ∈ V
23	21, 22	ndisjrelk 4323	. . . . . . . . . . . 12 ⊢ (⟪z, y⟫ ∈ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k ℘₁℘₁1_c) ↔ (z ∩ y) ≠ ∅)
24	23	necon2bbii 2572	. . . . . . . . . . 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 4256	. . . . . . . . . 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 3448	. . . . . . . . . . 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 4113	. . . . . . . . . . . . . 14 ⊢ ⟪{{z}}, ⟪y, x⟫⟫ ∈ V
32	31	elimak 4259	. . . . . . . . . . . . 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 2620	. . . . . . . . . . . . 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 4150	. . . . . . . . . . . . . . . . 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 4111	. . . . . . . . . . . . . . 15 ⊢ {{{{{w}}}}} ∈ V
43		opkeq1 4059	. . . . . . . . . . . . . . . 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 2894	. . . . . . . . . . . . . 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 3223	. . . . . . . . . . . . . 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 4111	. . . . . . . . . . . . . . . . . 18 ⊢ {{{w}}} ∈ V
48	47, 14, 4	otkelins2k 4255	. . . . . . . . . . . . . . . . 17 ⊢ (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ Ins2_k Ins2_k S_k ↔ ⟪{{{w}}}, ⟪y, x⟫⟫ ∈ Ins2_k S_k )
49		snex 4111	. . . . . . . . . . . . . . . . . 18 ⊢ {w} ∈ V
50	49, 22, 2	otkelins2k 4255	. . . . . . . . . . . . . . . . 17 ⊢ (⟪{{{w}}}, ⟪y, x⟫⟫ ∈ Ins2_k S_k ↔ ⟪{w}, x⟫ ∈ S_k )
51		vex 2862	. . . . . . . . . . . . . . . . . 18 ⊢ w ∈ V
52	51, 2	elssetk 4270	. . . . . . . . . . . . . . . . 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 4255	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ Ins2_k Ins3_k S_k ↔ ⟪{{{w}}}, ⟪y, x⟫⟫ ∈ Ins3_k S_k )
55	49, 22, 2	otkelins3k 4256	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟪{{{w}}}, ⟪y, x⟫⟫ ∈ Ins3_k S_k ↔ ⟪{w}, y⟫ ∈ S_k )
56	51, 22	elssetk 4270	. . . . . . . . . . . . . . . . . . 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 4256	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ∈ Ins3_k SI_k SI_k S_k ↔ ⟪{{{w}}}, {{z}}⟫ ∈ SI_k SI_k S_k )
59		snex 4111	. . . . . . . . . . . . . . . . . . . 20 ⊢ {{w}} ∈ V
60		snex 4111	. . . . . . . . . . . . . . . . . . . 20 ⊢ {z} ∈ V
61	59, 60	opksnelsik 4265	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟪{{{w}}}, {{z}}⟫ ∈ SI_k SI_k S_k ↔ ⟪{{w}}, {z}⟫ ∈ SI_k S_k )
62	49, 21	opksnelsik 4265	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟪{{w}}, {z}⟫ ∈ SI_k S_k ↔ ⟪{w}, z⟫ ∈ S_k )
63	51, 21	elssetk 4270	. . . . . . . . . . . . . . . . . . . 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 3220	. . . . . . . . . . . . . . . . 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 3220	. . . . . . . . . . . . . . . . 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 2639	. . . . . 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 2639	. . . 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 2464	. 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 2615 ∼ ccompl 3205 ∖ cdif 3206 ∪ cun 3207 ∩ cin 3208 ⊕ csymdif 3209 ∅c0 3550 {csn 3737 ⟪copk 4057 1_cc1c 4134 ℘₁cpw1 4135 Ins2_k cins2k 4176 Ins3_k cins3k 4177 “_k cimak 4179 SI_k csik 4181 S_k cssetk 4183 +_c cplc 4375

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 4078 ax-sn 4087

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 2478 df-ne 2518 df-rex 2620 df-v 2861 df-nin 3211 df-compl 3212 df-in 3213 df-un 3214 df-dif 3215 df-symdif 3216 df-ss 3259 df-nul 3551 df-pw 3724 df-sn 3741 df-pr 3742 df-opk 4058 df-1c 4136 df-pw1 4137 df-ins2k 4187 df-ins3k 4188 df-imak 4189 df-sik 4192 df-ssetk 4193 df-addc 4378

This theorem is referenced by: addceq1 4383 addceq2 4384 addcexg 4393 dfnnc2 4395 nnc0suc 4412 nncaddccl 4419 nnsucelrlem1 4424 preaddccan2lem1 4454 ltfinex 4464 evenodddisjlem1 4515 dfphi2 4569 phialllem1 4616

W3C validator