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

Theorem dfnnc2 4395
Description: Definition of the finite cardinals for existence theorem. (Contributed by SF, 14-Jan-2015.)
Assertion
Ref Expression
dfnnc2 Nn = ({x 0c x} (( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) “k 1c))

Proof of Theorem dfnnc2
Dummy variables y z w t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nnc 4379 . 2 Nn = {y (0c y z y (z +c 1c) y)}
2 eldif 3221 . . . . 5 (y ({x 0c x} (( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) “k 1c)) ↔ (y {x 0c x} ¬ y (( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) “k 1c)))
3 vex 2862 . . . . . . 7 y V
4 eleq2 2414 . . . . . . 7 (x = y → (0c x ↔ 0c y))
53, 4elab 2985 . . . . . 6 (y {x 0c x} ↔ 0c y)
6 snex 4111 . . . . . . . . . . . 12 {z} V
7 opkeq1 4059 . . . . . . . . . . . . 13 (t = {z} → ⟪t, y⟫ = ⟪{z}, y⟫)
87eleq1d 2419 . . . . . . . . . . . 12 (t = {z} → (⟪t, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) ↔ ⟪{z}, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))))
96, 8ceqsexv 2894 . . . . . . . . . . 11 (t(t = {z} t, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))) ↔ ⟪{z}, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))))
10 eldif 3221 . . . . . . . . . . . 12 (⟪{z}, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) ↔ (⟪{z}, y Sk ¬ ⟪{z}, y ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))))
11 vex 2862 . . . . . . . . . . . . . 14 z V
1211, 3elssetk 4270 . . . . . . . . . . . . 13 (⟪{z}, y Skz y)
13 snex 4111 . . . . . . . . . . . . . . . . . 18 {w} V
14 opkeq2 4060 . . . . . . . . . . . . . . . . . . . . 21 (t = {w} → ⟪{z}, t⟫ = ⟪{z}, {w}⟫)
1514eleq1d 2419 . . . . . . . . . . . . . . . . . . . 20 (t = {w} → (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ↔ ⟪{z}, {w}⟫ SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))
16 vex 2862 . . . . . . . . . . . . . . . . . . . . 21 w V
1711, 16opksnelsik 4265 . . . . . . . . . . . . . . . . . . . 20 (⟪{z}, {w}⟫ SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ↔ ⟪z, w Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))
1815, 17syl6bb 252 . . . . . . . . . . . . . . . . . . 19 (t = {w} → (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ↔ ⟪z, w Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))
19 opkeq1 4059 . . . . . . . . . . . . . . . . . . . 20 (t = {w} → ⟪t, y⟫ = ⟪{w}, y⟫)
2019eleq1d 2419 . . . . . . . . . . . . . . . . . . 19 (t = {w} → (⟪t, y Sk ↔ ⟪{w}, y Sk ))
2118, 20anbi12d 691 . . . . . . . . . . . . . . . . . 18 (t = {w} → ((⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk ) ↔ (⟪z, w Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ⟪{w}, y Sk )))
2213, 21ceqsexv 2894 . . . . . . . . . . . . . . . . 17 (t(t = {w} (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk )) ↔ (⟪z, w Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ⟪{w}, y Sk ))
23 opkelimagekg 4271 . . . . . . . . . . . . . . . . . . . 20 ((z V w V) → (⟪z, w Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ↔ w = ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k z)))
2411, 16, 23mp2an 653 . . . . . . . . . . . . . . . . . . 19 (⟪z, w Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ↔ w = ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k z))
25 dfaddc2 4381 . . . . . . . . . . . . . . . . . . . 20 (z +c 1c) = ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k z)
2625eqeq2i 2363 . . . . . . . . . . . . . . . . . . 19 (w = (z +c 1c) ↔ w = ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k z))
2724, 26bitr4i 243 . . . . . . . . . . . . . . . . . 18 (⟪z, w Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ↔ w = (z +c 1c))
2816, 3elssetk 4270 . . . . . . . . . . . . . . . . . 18 (⟪{w}, y Skw y)
2927, 28anbi12i 678 . . . . . . . . . . . . . . . . 17 ((⟪z, w Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ⟪{w}, y Sk ) ↔ (w = (z +c 1c) w y))
3022, 29bitri 240 . . . . . . . . . . . . . . . 16 (t(t = {w} (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk )) ↔ (w = (z +c 1c) w y))
3130exbii 1582 . . . . . . . . . . . . . . 15 (wt(t = {w} (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk )) ↔ w(w = (z +c 1c) w y))
326, 3opkelcok 4262 . . . . . . . . . . . . . . . 16 (⟪{z}, y ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) ↔ t(⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk ))
33 el1c 4139 . . . . . . . . . . . . . . . . . . . 20 (t 1cw t = {w})
3433anbi1i 676 . . . . . . . . . . . . . . . . . . 19 ((t 1c (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk )) ↔ (w t = {w} (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk )))
35 19.41v 1901 . . . . . . . . . . . . . . . . . . 19 (w(t = {w} (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk )) ↔ (w t = {w} (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk )))
3634, 35bitr4i 243 . . . . . . . . . . . . . . . . . 18 ((t 1c (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk )) ↔ w(t = {w} (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk )))
3736exbii 1582 . . . . . . . . . . . . . . . . 17 (t(t 1c (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk )) ↔ tw(t = {w} (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk )))
38 sikss1c1c 4267 . . . . . . . . . . . . . . . . . . . . . . 23 SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) (1c ×k 1c)
3938sseli 3269 . . . . . . . . . . . . . . . . . . . . . 22 (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) → ⟪{z}, t (1c ×k 1c))
40 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . 24 t V
416, 40opkelxpk 4248 . . . . . . . . . . . . . . . . . . . . . . 23 (⟪{z}, t (1c ×k 1c) ↔ ({z} 1c t 1c))
4241simprbi 450 . . . . . . . . . . . . . . . . . . . . . 22 (⟪{z}, t (1c ×k 1c) → t 1c)
4339, 42syl 15 . . . . . . . . . . . . . . . . . . . . 21 (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) → t 1c)
4443pm4.71ri 614 . . . . . . . . . . . . . . . . . . . 20 (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ↔ (t 1c ⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))
4544anbi1i 676 . . . . . . . . . . . . . . . . . . 19 ((⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk ) ↔ ((t 1c ⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) t, y Sk ))
46 anass 630 . . . . . . . . . . . . . . . . . . 19 (((t 1c ⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) t, y Sk ) ↔ (t 1c (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk )))
4745, 46bitri 240 . . . . . . . . . . . . . . . . . 18 ((⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk ) ↔ (t 1c (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk )))
4847exbii 1582 . . . . . . . . . . . . . . . . 17 (t(⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk ) ↔ t(t 1c (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk )))
49 excom 1741 . . . . . . . . . . . . . . . . 17 (wt(t = {w} (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk )) ↔ tw(t = {w} (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk )))
5037, 48, 493bitr4i 268 . . . . . . . . . . . . . . . 16 (t(⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk ) ↔ wt(t = {w} (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk )))
5132, 50bitri 240 . . . . . . . . . . . . . . 15 (⟪{z}, y ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) ↔ wt(t = {w} (⟪{z}, t SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) t, y Sk )))
52 df-clel 2349 . . . . . . . . . . . . . . 15 ((z +c 1c) yw(w = (z +c 1c) w y))
5331, 51, 523bitr4i 268 . . . . . . . . . . . . . 14 (⟪{z}, y ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) ↔ (z +c 1c) y)
5453notbii 287 . . . . . . . . . . . . 13 (¬ ⟪{z}, y ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)) ↔ ¬ (z +c 1c) y)
5512, 54anbi12i 678 . . . . . . . . . . . 12 ((⟪{z}, y Sk ¬ ⟪{z}, y ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) ↔ (z y ¬ (z +c 1c) y))
5610, 55bitri 240 . . . . . . . . . . 11 (⟪{z}, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) ↔ (z y ¬ (z +c 1c) y))
579, 56bitri 240 . . . . . . . . . 10 (t(t = {z} t, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))) ↔ (z y ¬ (z +c 1c) y))
5857exbii 1582 . . . . . . . . 9 (zt(t = {z} t, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))) ↔ z(z y ¬ (z +c 1c) y))
593elimak 4259 . . . . . . . . . 10 (y (( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) “k 1c) ↔ t 1ct, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))))
60 el1c 4139 . . . . . . . . . . . . . 14 (t 1cz t = {z})
6160anbi1i 676 . . . . . . . . . . . . 13 ((t 1c t, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))) ↔ (z t = {z} t, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))))
62 19.41v 1901 . . . . . . . . . . . . 13 (z(t = {z} t, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))) ↔ (z t = {z} t, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))))
6361, 62bitr4i 243 . . . . . . . . . . . 12 ((t 1c t, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))) ↔ z(t = {z} t, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))))
6463exbii 1582 . . . . . . . . . . 11 (t(t 1c t, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))) ↔ tz(t = {z} t, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))))
65 df-rex 2620 . . . . . . . . . . 11 (t 1ct, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) ↔ t(t 1c t, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))))
66 excom 1741 . . . . . . . . . . 11 (zt(t = {z} t, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))) ↔ tz(t = {z} t, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))))
6764, 65, 663bitr4i 268 . . . . . . . . . 10 (t 1ct, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) ↔ zt(t = {z} t, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))))
6859, 67bitri 240 . . . . . . . . 9 (y (( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) “k 1c) ↔ zt(t = {z} t, y ( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c)))))
69 df-rex 2620 . . . . . . . . 9 (z y ¬ (z +c 1c) yz(z y ¬ (z +c 1c) y))
7058, 68, 693bitr4i 268 . . . . . . . 8 (y (( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) “k 1c) ↔ z y ¬ (z +c 1c) y)
71 rexnal 2625 . . . . . . . 8 (z y ¬ (z +c 1c) y ↔ ¬ z y (z +c 1c) y)
7270, 71bitr2i 241 . . . . . . 7 z y (z +c 1c) yy (( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) “k 1c))
7372con1bii 321 . . . . . 6 y (( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) “k 1c) ↔ z y (z +c 1c) y)
745, 73anbi12i 678 . . . . 5 ((y {x 0c x} ¬ y (( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) “k 1c)) ↔ (0c y z y (z +c 1c) y))
752, 74bitri 240 . . . 4 (y ({x 0c x} (( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) “k 1c)) ↔ (0c y z y (z +c 1c) y))
7675abbi2i 2464 . . 3 ({x 0c x} (( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) “k 1c)) = {y (0c y z y (z +c 1c) y)}
7776inteqi 3930 . 2 ({x 0c x} (( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) “k 1c)) = {y (0c y z y (z +c 1c) y)}
781, 77eqtr4i 2376 1 Nn = ({x 0c x} (( Sk ( Sk k SIk Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))) “k 1c))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 176   wa 358  wex 1541   = wceq 1642   wcel 1710  {cab 2339  wral 2614  wrex 2615  Vcvv 2859  ccompl 3205   cdif 3206  cun 3207  cin 3208  csymdif 3209  {csn 3737  cint 3926  copk 4057  1cc1c 4134  1cpw1 4135   ×k cxpk 4174   Ins2k cins2k 4176   Ins3k cins3k 4177  k cimak 4179   k ccomk 4180   SIk csik 4181  Imagekcimagek 4182   Sk cssetk 4183   Nn cnnc 4373  0cc0c 4374   +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-ral 2619  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-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-addc 4378  df-nnc 4379
This theorem is referenced by:  nncex  4396
  Copyright terms: Public domain W3C validator