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

 Description: Alternate definition of cardinal addition to establish stratification. (Contributed by SF, 15-Jan-2015.)
Assertion
Ref Expression
dfaddc2 (A +c B) = ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 11B) “k A)

Dummy variables x y z t w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-addc 4378 . 2 (A +c B) = {x y A z B ((yz) = x = (yz))}
2 vex 2862 . . . . 5 x V
32elimak 4259 . . . 4 (x ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 11B) “k A) ↔ y Ay, x (( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 11B))
4 opkex 4113 . . . . . . 7 y, x V
54elimak 4259 . . . . . 6 (⟪y, x (( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 11B) ↔ t 1 1Bt, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)))
6 elpw12 4145 . . . . . . . . . 10 (t 11Bz B t = {{z}})
76anbi1i 676 . . . . . . . . 9 ((t 11B t, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c))) ↔ (z B t = {{z}} t, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c))))
8 r19.41v 2764 . . . . . . . . 9 (z B (t = {{z}} t, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c))) ↔ (z B t = {{z}} t, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c))))
97, 8bitr4i 243 . . . . . . . 8 ((t 11B t, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c))) ↔ z B (t = {{z}} t, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c))))
109exbii 1582 . . . . . . 7 (t(t 11B t, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c))) ↔ tz B (t = {{z}} t, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c))))
11 df-rex 2620 . . . . . . 7 (t 1 1Bt, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) ↔ t(t 11B t, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c))))
12 rexcom4 2878 . . . . . . 7 (z B t(t = {{z}} t, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c))) ↔ tz B (t = {{z}} t, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c))))
1310, 11, 123bitr4i 268 . . . . . 6 (t 1 1Bt, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) ↔ z B t(t = {{z}} t, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c))))
14 snex 4111 . . . . . . . . 9 {{z}} V
15 opkeq1 4059 . . . . . . . . . 10 (t = {{z}} → ⟪t, ⟪y, x⟫⟫ = ⟪{{z}}, ⟪y, x⟫⟫)
1615eleq1d 2419 . . . . . . . . 9 (t = {{z}} → (⟪t, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) ↔ ⟪{{z}}, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c))))
1714, 16ceqsexv 2894 . . . . . . . 8 (t(t = {{z}} t, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c))) ↔ ⟪{{z}}, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)))
18 eldif 3221 . . . . . . . 8 (⟪{{z}}, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) ↔ (⟪{{z}}, ⟪y, x⟫⟫ Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) ¬ ⟪{{z}}, ⟪y, x⟫⟫ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)))
19 opkex 4113 . . . . . . . . . . . 12 z, y V
2019elcompl 3225 . . . . . . . . . . 11 (⟪z, y ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ¬ ⟪z, y (( Ins3k SkIns2k Sk ) “k 111c))
21 vex 2862 . . . . . . . . . . . . 13 z V
22 vex 2862 . . . . . . . . . . . . 13 y V
2321, 22ndisjrelk 4323 . . . . . . . . . . . 12 (⟪z, y (( Ins3k SkIns2k Sk ) “k 111c) ↔ (zy) ≠ )
2423necon2bbii 2572 . . . . . . . . . . 11 ((zy) = ↔ ¬ ⟪z, y (( Ins3k SkIns2k Sk ) “k 111c))
2520, 24bitr4i 243 . . . . . . . . . 10 (⟪z, y ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ (zy) = )
2621, 22, 2otkelins3k 4256 . . . . . . . . . 10 (⟪{{z}}, ⟪y, x⟫⟫ Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ ⟪z, y ∼ (( Ins3k SkIns2k Sk ) “k 111c))
27 incom 3448 . . . . . . . . . . 11 (yz) = (zy)
2827eqeq1i 2360 . . . . . . . . . 10 ((yz) = ↔ (zy) = )
2925, 26, 283bitr4i 268 . . . . . . . . 9 (⟪{{z}}, ⟪y, x⟫⟫ Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) ↔ (yz) = )
30 dfcleq 2347 . . . . . . . . . 10 (x = (yz) ↔ w(w xw (yz)))
31 opkex 4113 . . . . . . . . . . . . . 14 ⟪{{z}}, ⟪y, x⟫⟫ V
3231elimak 4259 . . . . . . . . . . . . 13 (⟪{{z}}, ⟪y, x⟫⟫ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c) ↔ t 1 1111ct, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )))
33 df-rex 2620 . . . . . . . . . . . . 13 (t 1 1111ct, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) ↔ t(t 11111c t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk ))))
34 elpw141c 4150 . . . . . . . . . . . . . . . . 17 (t 11111cw t = {{{{{w}}}}})
3534anbi1i 676 . . . . . . . . . . . . . . . 16 ((t 11111c t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk ))) ↔ (w t = {{{{{w}}}}} t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk ))))
36 19.41v 1901 . . . . . . . . . . . . . . . 16 (w(t = {{{{{w}}}}} t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk ))) ↔ (w t = {{{{{w}}}}} t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk ))))
3735, 36bitr4i 243 . . . . . . . . . . . . . . 15 ((t 11111c t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk ))) ↔ w(t = {{{{{w}}}}} t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk ))))
3837exbii 1582 . . . . . . . . . . . . . 14 (t(t 11111c t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk ))) ↔ tw(t = {{{{{w}}}}} t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk ))))
39 excom 1741 . . . . . . . . . . . . . 14 (wt(t = {{{{{w}}}}} t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk ))) ↔ tw(t = {{{{{w}}}}} t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk ))))
4038, 39bitr4i 243 . . . . . . . . . . . . 13 (t(t 11111c t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk ))) ↔ wt(t = {{{{{w}}}}} t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk ))))
4132, 33, 403bitri 262 . . . . . . . . . . . 12 (⟪{{z}}, ⟪y, x⟫⟫ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c) ↔ wt(t = {{{{{w}}}}} t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk ))))
42 snex 4111 . . . . . . . . . . . . . . 15 {{{{{w}}}}} V
43 opkeq1 4059 . . . . . . . . . . . . . . . 16 (t = {{{{{w}}}}} → ⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ = ⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫)
4443eleq1d 2419 . . . . . . . . . . . . . . 15 (t = {{{{{w}}}}} → (⟪t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) ↔ ⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk ))))
4542, 44ceqsexv 2894 . . . . . . . . . . . . . 14 (t(t = {{{{{w}}}}} t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk ))) ↔ ⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )))
46 elsymdif 3223 . . . . . . . . . . . . . 14 (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) ↔ ¬ (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ Ins2k Ins2k Sk ↔ ⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins3k SkIns3k SIk SIk Sk )))
47 snex 4111 . . . . . . . . . . . . . . . . . 18 {{{w}}} V
4847, 14, 4otkelins2k 4255 . . . . . . . . . . . . . . . . 17 (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ Ins2k Ins2k Sk ↔ ⟪{{{w}}}, ⟪y, x⟫⟫ Ins2k Sk )
49 snex 4111 . . . . . . . . . . . . . . . . . 18 {w} V
5049, 22, 2otkelins2k 4255 . . . . . . . . . . . . . . . . 17 (⟪{{{w}}}, ⟪y, x⟫⟫ Ins2k Sk ↔ ⟪{w}, x Sk )
51 vex 2862 . . . . . . . . . . . . . . . . . 18 w V
5251, 2elssetk 4270 . . . . . . . . . . . . . . . . 17 (⟪{w}, x Skw x)
5348, 50, 523bitri 262 . . . . . . . . . . . . . . . 16 (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ Ins2k Ins2k Skw x)
5447, 14, 4otkelins2k 4255 . . . . . . . . . . . . . . . . . . 19 (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ Ins2k Ins3k Sk ↔ ⟪{{{w}}}, ⟪y, x⟫⟫ Ins3k Sk )
5549, 22, 2otkelins3k 4256 . . . . . . . . . . . . . . . . . . 19 (⟪{{{w}}}, ⟪y, x⟫⟫ Ins3k Sk ↔ ⟪{w}, y Sk )
5651, 22elssetk 4270 . . . . . . . . . . . . . . . . . . 19 (⟪{w}, y Skw y)
5754, 55, 563bitri 262 . . . . . . . . . . . . . . . . . 18 (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ Ins2k Ins3k Skw y)
5847, 14, 4otkelins3k 4256 . . . . . . . . . . . . . . . . . . 19 (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ Ins3k SIk SIk Sk ↔ ⟪{{{w}}}, {{z}}⟫ SIk SIk Sk )
59 snex 4111 . . . . . . . . . . . . . . . . . . . 20 {{w}} V
60 snex 4111 . . . . . . . . . . . . . . . . . . . 20 {z} V
6159, 60opksnelsik 4265 . . . . . . . . . . . . . . . . . . 19 (⟪{{{w}}}, {{z}}⟫ SIk SIk Sk ↔ ⟪{{w}}, {z}⟫ SIk Sk )
6249, 21opksnelsik 4265 . . . . . . . . . . . . . . . . . . . 20 (⟪{{w}}, {z}⟫ SIk Sk ↔ ⟪{w}, z Sk )
6351, 21elssetk 4270 . . . . . . . . . . . . . . . . . . . 20 (⟪{w}, z Skw z)
6462, 63bitri 240 . . . . . . . . . . . . . . . . . . 19 (⟪{{w}}, {z}⟫ SIk Skw z)
6558, 61, 643bitri 262 . . . . . . . . . . . . . . . . . 18 (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ Ins3k SIk SIk Skw z)
6657, 65orbi12i 507 . . . . . . . . . . . . . . . . 17 ((⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ Ins2k Ins3k Sk ⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ Ins3k SIk SIk Sk ) ↔ (w y w z))
67 elun 3220 . . . . . . . . . . . . . . . . 17 (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins3k SkIns3k SIk SIk Sk ) ↔ (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ Ins2k Ins3k Sk ⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ Ins3k SIk SIk Sk ))
68 elun 3220 . . . . . . . . . . . . . . . . 17 (w (yz) ↔ (w y w z))
6966, 67, 683bitr4i 268 . . . . . . . . . . . . . . . 16 (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins3k SkIns3k SIk SIk Sk ) ↔ w (yz))
7053, 69bibi12i 306 . . . . . . . . . . . . . . 15 ((⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ Ins2k Ins2k Sk ↔ ⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) ↔ (w xw (yz)))
7170notbii 287 . . . . . . . . . . . . . 14 (¬ (⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ Ins2k Ins2k Sk ↔ ⟪{{{{{w}}}}}, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) ↔ ¬ (w xw (yz)))
7245, 46, 713bitri 262 . . . . . . . . . . . . 13 (t(t = {{{{{w}}}}} t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk ))) ↔ ¬ (w xw (yz)))
7372exbii 1582 . . . . . . . . . . . 12 (wt(t = {{{{{w}}}}} t, ⟪{{z}}, ⟪y, x⟫⟫⟫ ( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk ))) ↔ w ¬ (w xw (yz)))
74 exnal 1574 . . . . . . . . . . . 12 (w ¬ (w xw (yz)) ↔ ¬ w(w xw (yz)))
7541, 73, 743bitri 262 . . . . . . . . . . 11 (⟪{{z}}, ⟪y, x⟫⟫ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c) ↔ ¬ w(w xw (yz)))
7675con2bii 322 . . . . . . . . . 10 (w(w xw (yz)) ↔ ¬ ⟪{{z}}, ⟪y, x⟫⟫ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c))
7730, 76bitr2i 241 . . . . . . . . 9 (¬ ⟪{{z}}, ⟪y, x⟫⟫ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c) ↔ x = (yz))
7829, 77anbi12i 678 . . . . . . . 8 ((⟪{{z}}, ⟪y, x⟫⟫ Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) ¬ ⟪{{z}}, ⟪y, x⟫⟫ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) ↔ ((yz) = x = (yz)))
7917, 18, 783bitri 262 . . . . . . 7 (t(t = {{z}} t, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c))) ↔ ((yz) = x = (yz)))
8079rexbii 2639 . . . . . 6 (z B t(t = {{z}} t, ⟪y, x⟫⟫ ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c))) ↔ z B ((yz) = x = (yz)))
815, 13, 803bitri 262 . . . . 5 (⟪y, x (( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 11B) ↔ z B ((yz) = x = (yz)))
8281rexbii 2639 . . . 4 (y Ay, x (( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 11B) ↔ y A z B ((yz) = x = (yz)))
833, 82bitri 240 . . 3 (x ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 11B) “k A) ↔ y A z B ((yz) = x = (yz)))
8483abbi2i 2464 . 2 ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 11B) “k A) = {x y A z B ((yz) = x = (yz))}
851, 84eqtr4i 2376 1 (A +c B) = ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 11B) “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  1cc1c 4134  ℘1cpw1 4135   Ins2k cins2k 4176   Ins3k cins3k 4177   “k cimak 4179   SIk csik 4181   Sk cssetk 4183   +c cplc 4375 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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
 Copyright terms: Public domain W3C validator