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

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

Proof of Theorem spfinex
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-spfin 4446 . . 3 Spfin Ncfin Sfin
2 vex 2862 . . . . . . . . . . . 12
32elimak 4259 . . . . . . . . . . 11 SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1ck1c 1c SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c
4 el1c 4139 . . . . . . . . . . . . . . 15 1c
54anbi1i 676 . . . . . . . . . . . . . 14 1c SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c
6 19.41v 1901 . . . . . . . . . . . . . 14 SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c
75, 6bitr4i 243 . . . . . . . . . . . . 13 1c SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c
87exbii 1582 . . . . . . . . . . . 12 1c SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c
9 df-rex 2620 . . . . . . . . . . . 12 1c SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c 1c SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c
10 excom 1741 . . . . . . . . . . . 12 SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c
118, 9, 103bitr4i 268 . . . . . . . . . . 11 1c SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c
12 snex 4111 . . . . . . . . . . . . . 14
13 opkeq1 4059 . . . . . . . . . . . . . . 15
1413eleq1d 2419 . . . . . . . . . . . . . 14 SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c
1512, 14ceqsexv 2894 . . . . . . . . . . . . 13 SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c
16 elin 3219 . . . . . . . . . . . . 13 SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c
17 vex 2862 . . . . . . . . . . . . . . 15
1817, 2elssetk 4270 . . . . . . . . . . . . . 14 SSetk
19 opkex 4113 . . . . . . . . . . . . . . . . 17
2019elimak 4259 . . . . . . . . . . . . . . . 16 Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c 1 1 1c Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk
21 df-rex 2620 . . . . . . . . . . . . . . . 16 1 1 1c Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk 1 1 1c Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk
22 elpw121c 4148 . . . . . . . . . . . . . . . . . . . 20 1 1 1c
2322anbi1i 676 . . . . . . . . . . . . . . . . . . 19 1 1 1c Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk
24 19.41v 1901 . . . . . . . . . . . . . . . . . . 19 Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk
2523, 24bitr4i 243 . . . . . . . . . . . . . . . . . 18 1 1 1c Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk
2625exbii 1582 . . . . . . . . . . . . . . . . 17 1 1 1c Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk
27 excom 1741 . . . . . . . . . . . . . . . . 17 Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk
2826, 27bitr4i 243 . . . . . . . . . . . . . . . 16 1 1 1c Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk
2920, 21, 283bitri 262 . . . . . . . . . . . . . . 15 Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk
30 snex 4111 . . . . . . . . . . . . . . . . . 18
31 opkeq1 4059 . . . . . . . . . . . . . . . . . . 19
3231eleq1d 2419 . . . . . . . . . . . . . . . . . 18 Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk
3330, 32ceqsexv 2894 . . . . . . . . . . . . . . . . 17 Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk
34 eldif 3221 . . . . . . . . . . . . . . . . 17 Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk
35 snex 4111 . . . . . . . . . . . . . . . . . . . 20
3635, 12, 2otkelins3k 4256 . . . . . . . . . . . . . . . . . . 19 Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c
37 vex 2862 . . . . . . . . . . . . . . . . . . . 20
3837, 17opksnelsik 4265 . . . . . . . . . . . . . . . . . . 19 SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c
3937, 17srelk 4524 . . . . . . . . . . . . . . . . . . 19 Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Sfin
4036, 38, 393bitri 262 . . . . . . . . . . . . . . . . . 18 Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Sfin
4135, 12, 2otkelins2k 4255 . . . . . . . . . . . . . . . . . . . 20 Ins2k SSetk SSetk
4237, 2elssetk 4270 . . . . . . . . . . . . . . . . . . . 20 SSetk
4341, 42bitri 240 . . . . . . . . . . . . . . . . . . 19 Ins2k SSetk
4443notbii 287 . . . . . . . . . . . . . . . . . 18 Ins2k SSetk
4540, 44anbi12i 678 . . . . . . . . . . . . . . . . 17 Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk Sfin
4633, 34, 453bitri 262 . . . . . . . . . . . . . . . 16 Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk Sfin
4746exbii 1582 . . . . . . . . . . . . . . 15 Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk Sfin
48 exanali 1585 . . . . . . . . . . . . . . 15 Sfin Sfin
4929, 47, 483bitri 262 . . . . . . . . . . . . . 14 Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c Sfin
5018, 49anbi12i 678 . . . . . . . . . . . . 13 SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c Sfin
5115, 16, 503bitri 262 . . . . . . . . . . . 12 SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c Sfin
5251exbii 1582 . . . . . . . . . . 11 SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c Sfin
533, 11, 523bitri 262 . . . . . . . . . 10 SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1ck1c Sfin
54 df-rex 2620 . . . . . . . . . 10 Sfin Sfin
5553, 54bitr4i 243 . . . . . . . . 9 SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1ck1c Sfin
5655notbii 287 . . . . . . . 8 SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1ck1c Sfin
572elcompl 3225 . . . . . . . 8 SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1ck1c SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1ck1c
58 dfral2 2626 . . . . . . . 8 Sfin Sfin
5956, 57, 583bitr4i 268 . . . . . . 7 SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1ck1c Sfin
6059abbi2i 2464 . . . . . 6 SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1ck1c Sfin
6160ineq2i 3454 . . . . 5 Ncfin SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1ck1c Ncfin Sfin
62 inab 3522 . . . . 5 Ncfin Sfin Ncfin Sfin
6361, 62eqtri 2373 . . . 4 Ncfin SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1ck1c Ncfin Sfin
6463inteqi 3930 . . 3 Ncfin SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1ck1c Ncfin Sfin
651, 64eqtr4i 2376 . 2 Spfin Ncfin SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1ck1c
66 setswithex 4322 . . . 4 Ncfin
67 ssetkex 4294 . . . . . . 7 SSetk
68 srelkex 4525 . . . . . . . . . . 11 Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c
6968sikex 4297 . . . . . . . . . 10 SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c
7069ins3kex 4308 . . . . . . . . 9 Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c
7167ins2kex 4307 . . . . . . . . 9 Ins2k SSetk
7270, 71difex 4107 . . . . . . . 8 Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk
73 1cex 4142 . . . . . . . . . 10 1c
7473pw1ex 4303 . . . . . . . . 9 1 1c
7574pw1ex 4303 . . . . . . . 8 1 1 1c
7672, 75imakex 4300 . . . . . . 7 Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c
7767, 76inex 4105 . . . . . 6 SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1c
7877, 73imakex 4300 . . . . 5 SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1ck1c
7978complex 4104 . . . 4 SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1ck1c
8066, 79inex 4105 . . 3 Ncfin SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1ck1c
8180intex 4320 . 2 Ncfin SSetk Ins3k SIk Nn k Nn Ins3k Ins3k SIk 1c k Ins3k SSetk Ins2k SIk SSetk k1 1 1 1c Ins2k SSetk k1 1 1c Ins2k Ins3k SIk Ins3k SSetk Ins2k SIk SSetk k1 1 1c Ins2k SSetk k1 1 1ck1 1 1 1c Ins2k SSetk k1 1 1ck1c
8265, 81eqeltri 2423 1 Spfin
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wa 358  wal 1540  wex 1541   wceq 1642   wcel 1710  cab 2339  wral 2614  wrex 2615  cvv 2859   ∼ ccompl 3205   cdif 3206   cin 3208   csymdif 3209  cpw 3722  csn 3737  cint 3926  copk 4057  1cc1c 4134  1 cpw1 4135   k cxpk 4174   Ins2k cins2k 4176   Ins3k cins3k 4177  kcimak 4179   SIk csik 4181   SSetk cssetk 4183   Nn cnnc 4373   Ncfin cncfin 4433   Sfin wsfin 4437   Spfin cspfin 4438
This theorem is referenced by:  spfininduct  4540  vfinspss  4551  vfinspclt  4552  vfinncsp  4554  vinf  4555
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-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 4445  df-spfin 4446
  Copyright terms: Public domain W3C validator