NFE Home 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