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

Theorem spfinex 4537
 Description: Spfin is a set. (Contributed by SF, 20-Jan-2015.)
Assertion
Ref Expression
spfinex Spfin V

Proof of Theorem spfinex
Dummy variables x a z t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-spfin 4447 . . 3 Spfin = {a ( Ncfin V a x a z( Sfin (z, x) → z a))}
2 vex 2862 . . . . . . . . . . . 12 a V
32elimak 4259 . . . . . . . . . . 11 (a (( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) “k 1c) ↔ t 1ct, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)))
4 el1c 4139 . . . . . . . . . . . . . . 15 (t 1cx t = {x})
54anbi1i 676 . . . . . . . . . . . . . 14 ((t 1c t, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c))) ↔ (x t = {x} t, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c))))
6 19.41v 1901 . . . . . . . . . . . . . 14 (x(t = {x} t, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c))) ↔ (x t = {x} t, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c))))
75, 6bitr4i 243 . . . . . . . . . . . . 13 ((t 1c t, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c))) ↔ x(t = {x} t, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c))))
87exbii 1582 . . . . . . . . . . . 12 (t(t 1c t, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c))) ↔ tx(t = {x} t, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c))))
9 df-rex 2620 . . . . . . . . . . . 12 (t 1ct, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) ↔ t(t 1c t, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c))))
10 excom 1741 . . . . . . . . . . . 12 (xt(t = {x} t, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c))) ↔ tx(t = {x} t, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c))))
118, 9, 103bitr4i 268 . . . . . . . . . . 11 (t 1ct, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) ↔ xt(t = {x} t, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c))))
12 snex 4111 . . . . . . . . . . . . . 14 {x} V
13 opkeq1 4059 . . . . . . . . . . . . . . 15 (t = {x} → ⟪t, a⟫ = ⟪{x}, a⟫)
1413eleq1d 2419 . . . . . . . . . . . . . 14 (t = {x} → (⟪t, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) ↔ ⟪{x}, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c))))
1512, 14ceqsexv 2894 . . . . . . . . . . . . 13 (t(t = {x} t, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c))) ↔ ⟪{x}, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)))
16 elin 3219 . . . . . . . . . . . . 13 (⟪{x}, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) ↔ (⟪{x}, a Sk ⟪{x}, a (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)))
17 vex 2862 . . . . . . . . . . . . . . 15 x V
1817, 2elssetk 4270 . . . . . . . . . . . . . 14 (⟪{x}, a Skx a)
19 opkex 4113 . . . . . . . . . . . . . . . . 17 ⟪{x}, a V
2019elimak 4259 . . . . . . . . . . . . . . . 16 (⟪{x}, a (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c) ↔ t 1 11ct, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ))
21 df-rex 2620 . . . . . . . . . . . . . . . 16 (t 1 11ct, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) ↔ t(t 111c t, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk )))
22 elpw121c 4148 . . . . . . . . . . . . . . . . . . . 20 (t 111cz t = {{{z}}})
2322anbi1i 676 . . . . . . . . . . . . . . . . . . 19 ((t 111c t, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk )) ↔ (z t = {{{z}}} t, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk )))
24 19.41v 1901 . . . . . . . . . . . . . . . . . . 19 (z(t = {{{z}}} t, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk )) ↔ (z t = {{{z}}} t, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk )))
2523, 24bitr4i 243 . . . . . . . . . . . . . . . . . 18 ((t 111c t, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk )) ↔ z(t = {{{z}}} t, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk )))
2625exbii 1582 . . . . . . . . . . . . . . . . 17 (t(t 111c t, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk )) ↔ tz(t = {{{z}}} t, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk )))
27 excom 1741 . . . . . . . . . . . . . . . . 17 (zt(t = {{{z}}} t, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk )) ↔ tz(t = {{{z}}} t, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk )))
2826, 27bitr4i 243 . . . . . . . . . . . . . . . 16 (t(t 111c t, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk )) ↔ zt(t = {{{z}}} t, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk )))
2920, 21, 283bitri 262 . . . . . . . . . . . . . . 15 (⟪{x}, a (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c) ↔ zt(t = {{{z}}} t, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk )))
30 snex 4111 . . . . . . . . . . . . . . . . . 18 {{{z}}} V
31 opkeq1 4059 . . . . . . . . . . . . . . . . . . 19 (t = {{{z}}} → ⟪t, ⟪{x}, a⟫⟫ = ⟪{{{z}}}, ⟪{x}, a⟫⟫)
3231eleq1d 2419 . . . . . . . . . . . . . . . . . 18 (t = {{{z}}} → (⟪t, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) ↔ ⟪{{{z}}}, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk )))
3330, 32ceqsexv 2894 . . . . . . . . . . . . . . . . 17 (t(t = {{{z}}} t, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk )) ↔ ⟪{{{z}}}, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ))
34 eldif 3221 . . . . . . . . . . . . . . . . 17 (⟪{{{z}}}, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) ↔ (⟪{{{z}}}, ⟪{x}, a⟫⟫ Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ¬ ⟪{{{z}}}, ⟪{x}, a⟫⟫ Ins2k Sk ))
35 snex 4111 . . . . . . . . . . . . . . . . . . . 20 {z} V
3635, 12, 2otkelins3k 4256 . . . . . . . . . . . . . . . . . . 19 (⟪{{{z}}}, ⟪{x}, a⟫⟫ Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ ⟪{z}, {x}⟫ SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))
37 vex 2862 . . . . . . . . . . . . . . . . . . . 20 z V
3837, 17opksnelsik 4265 . . . . . . . . . . . . . . . . . . 19 (⟪{z}, {x}⟫ SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ ⟪z, x (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)))
3937, 17srelk 4524 . . . . . . . . . . . . . . . . . . 19 (⟪z, x (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ Sfin (z, x))
4036, 38, 393bitri 262 . . . . . . . . . . . . . . . . . 18 (⟪{{{z}}}, ⟪{x}, a⟫⟫ Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ Sfin (z, x))
4135, 12, 2otkelins2k 4255 . . . . . . . . . . . . . . . . . . . 20 (⟪{{{z}}}, ⟪{x}, a⟫⟫ Ins2k Sk ↔ ⟪{z}, a Sk )
4237, 2elssetk 4270 . . . . . . . . . . . . . . . . . . . 20 (⟪{z}, a Skz a)
4341, 42bitri 240 . . . . . . . . . . . . . . . . . . 19 (⟪{{{z}}}, ⟪{x}, a⟫⟫ Ins2k Skz a)
4443notbii 287 . . . . . . . . . . . . . . . . . 18 (¬ ⟪{{{z}}}, ⟪{x}, a⟫⟫ Ins2k Sk ↔ ¬ z a)
4540, 44anbi12i 678 . . . . . . . . . . . . . . . . 17 ((⟪{{{z}}}, ⟪{x}, a⟫⟫ Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ¬ ⟪{{{z}}}, ⟪{x}, a⟫⟫ Ins2k Sk ) ↔ ( Sfin (z, x) ¬ z a))
4633, 34, 453bitri 262 . . . . . . . . . . . . . . . 16 (t(t = {{{z}}} t, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk )) ↔ ( Sfin (z, x) ¬ z a))
4746exbii 1582 . . . . . . . . . . . . . . 15 (zt(t = {{{z}}} t, ⟪{x}, a⟫⟫ ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk )) ↔ z( Sfin (z, x) ¬ z a))
48 exanali 1585 . . . . . . . . . . . . . . 15 (z( Sfin (z, x) ¬ z a) ↔ ¬ z( Sfin (z, x) → z a))
4929, 47, 483bitri 262 . . . . . . . . . . . . . 14 (⟪{x}, a (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c) ↔ ¬ z( Sfin (z, x) → z a))
5018, 49anbi12i 678 . . . . . . . . . . . . 13 ((⟪{x}, a Sk ⟪{x}, a (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) ↔ (x a ¬ z( Sfin (z, x) → z a)))
5115, 16, 503bitri 262 . . . . . . . . . . . 12 (t(t = {x} t, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c))) ↔ (x a ¬ z( Sfin (z, x) → z a)))
5251exbii 1582 . . . . . . . . . . 11 (xt(t = {x} t, a ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c))) ↔ x(x a ¬ z( Sfin (z, x) → z a)))
533, 11, 523bitri 262 . . . . . . . . . 10 (a (( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) “k 1c) ↔ x(x a ¬ z( Sfin (z, x) → z a)))
54 df-rex 2620 . . . . . . . . . 10 (x a ¬ z( Sfin (z, x) → z a) ↔ x(x a ¬ z( Sfin (z, x) → z a)))
5553, 54bitr4i 243 . . . . . . . . 9 (a (( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) “k 1c) ↔ x a ¬ z( Sfin (z, x) → z a))
5655notbii 287 . . . . . . . 8 a (( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) “k 1c) ↔ ¬ x a ¬ z( Sfin (z, x) → z a))
572elcompl 3225 . . . . . . . 8 (a ∼ (( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) “k 1c) ↔ ¬ a (( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) “k 1c))
58 dfral2 2626 . . . . . . . 8 (x a z( Sfin (z, x) → z a) ↔ ¬ x a ¬ z( Sfin (z, x) → z a))
5956, 57, 583bitr4i 268 . . . . . . 7 (a ∼ (( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) “k 1c) ↔ x a z( Sfin (z, x) → z a))
6059abbi2i 2464 . . . . . 6 ∼ (( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) “k 1c) = {a x a z( Sfin (z, x) → z a)}
6160ineq2i 3454 . . . . 5 ({a Ncfin V a} ∩ ∼ (( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) “k 1c)) = ({a Ncfin V a} ∩ {a x a z( Sfin (z, x) → z a)})
62 inab 3522 . . . . 5 ({a Ncfin V a} ∩ {a x a z( Sfin (z, x) → z a)}) = {a ( Ncfin V a x a z( Sfin (z, x) → z a))}
6361, 62eqtri 2373 . . . 4 ({a Ncfin V a} ∩ ∼ (( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) “k 1c)) = {a ( Ncfin V a x a z( Sfin (z, x) → z a))}
6463inteqi 3930 . . 3 ({a Ncfin V a} ∩ ∼ (( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) “k 1c)) = {a ( Ncfin V a x a z( Sfin (z, x) → z a))}
651, 64eqtr4i 2376 . 2 Spfin = ({a Ncfin V a} ∩ ∼ (( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) “k 1c))
66 setswithex 4322 . . . 4 {a Ncfin V a} V
67 ssetkex 4294 . . . . . . 7 Sk V
68 srelkex 4525 . . . . . . . . . . 11 (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) V
6968sikex 4297 . . . . . . . . . 10 SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) V
7069ins3kex 4308 . . . . . . . . 9 Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) V
7167ins2kex 4307 . . . . . . . . 9 Ins2k Sk V
7270, 71difex 4107 . . . . . . . 8 ( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) V
73 1cex 4142 . . . . . . . . . 10 1c V
7473pw1ex 4303 . . . . . . . . 9 11c V
7574pw1ex 4303 . . . . . . . 8 111c V
7672, 75imakex 4300 . . . . . . 7 (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c) V
7767, 76inex 4105 . . . . . 6 ( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) V
7877, 73imakex 4300 . . . . 5 (( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) “k 1c) V
7978complex 4104 . . . 4 ∼ (( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) “k 1c) V
8066, 79inex 4105 . . 3 ({a Ncfin V a} ∩ ∼ (( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) “k 1c)) V
8180intex 4320 . 2 ({a Ncfin V a} ∩ ∼ (( Sk ∩ (( Ins3k SIk (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) Ins2k Sk ) “k 111c)) “k 1c)) V
8265, 81eqeltri 2423 1 Spfin V
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339  ∀wral 2614  ∃wrex 2615  Vcvv 2859   ∼ ccompl 3205   ∖ cdif 3206   ∩ cin 3208   ⊕ csymdif 3209  ℘cpw 3722  {csn 3737  ∩cint 3926  ⟪copk 4057  1cc1c 4134  ℘1cpw1 4135   ×k cxpk 4174   Ins2k cins2k 4176   Ins3k cins3k 4177   “k cimak 4179   SIk csik 4181   Sk cssetk 4183   Nn cnnc 4373   Ncfin cncfin 4434   Sfin wsfin 4438   Spfin cspfin 4439 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-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  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-sbc 3047  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-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-addc 4378  df-nnc 4379  df-sfin 4446  df-spfin 4447 This theorem is referenced by:  spfininduct  4540  vfinspss  4551  vfinspclt  4552  vfinncsp  4554  vinf  4555
 Copyright terms: Public domain W3C validator