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

Theorem ncfinlowerlem1 4482
Description: Lemma for ncfinlower 4483. Set up stratification for induction. (Contributed by SF, 22-Jan-2015.)
Assertion
Ref Expression
ncfinlowerlem1 1 1 Nn
Distinct variable group:   ,,,

Proof of Theorem ncfinlowerlem1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2862 . . . . . . 7
21elimak 4259 . . . . . 6 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1ck1 1c 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c
3 elpw11c 4147 . . . . . . . . . 10 1 1c
43anbi1i 676 . . . . . . . . 9 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c
5 19.41v 1901 . . . . . . . . 9 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c
64, 5bitr4i 243 . . . . . . . 8 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c
76exbii 1582 . . . . . . 7 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c
8 df-rex 2620 . . . . . . 7 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c
9 excom 1741 . . . . . . 7 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c
107, 8, 93bitr4i 268 . . . . . 6 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c
11 snex 4111 . . . . . . . . 9
12 opkeq1 4059 . . . . . . . . . 10
1312eleq1d 2419 . . . . . . . . 9 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c
1411, 13ceqsexv 2894 . . . . . . . 8 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c
15 opkex 4113 . . . . . . . . . 10
1615elimak 4259 . . . . . . . . 9 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c 1 1 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn
17 elpw131c 4149 . . . . . . . . . . . . 13 1 1 1 1c
1817anbi1i 676 . . . . . . . . . . . 12 1 1 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn
19 19.41v 1901 . . . . . . . . . . . 12 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn
2018, 19bitr4i 243 . . . . . . . . . . 11 1 1 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn
2120exbii 1582 . . . . . . . . . 10 1 1 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn
22 df-rex 2620 . . . . . . . . . 10 1 1 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn 1 1 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn
23 excom 1741 . . . . . . . . . 10 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn
2421, 22, 233bitr4i 268 . . . . . . . . 9 1 1 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn
25 snex 4111 . . . . . . . . . . . 12
26 opkeq1 4059 . . . . . . . . . . . . 13
2726eleq1d 2419 . . . . . . . . . . . 12 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn
2825, 27ceqsexv 2894 . . . . . . . . . . 11 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn
29 eldif 3221 . . . . . . . . . . 11 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn
30 elin 3219 . . . . . . . . . . . . 13 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c
3115elimak 4259 . . . . . . . . . . . . . . . 16 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c 1 1 1c Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
32 elpw121c 4148 . . . . . . . . . . . . . . . . . . . 20 1 1 1c
3332anbi1i 676 . . . . . . . . . . . . . . . . . . 19 1 1 1c Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
34 19.41v 1901 . . . . . . . . . . . . . . . . . . 19 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
3533, 34bitr4i 243 . . . . . . . . . . . . . . . . . 18 1 1 1c Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
3635exbii 1582 . . . . . . . . . . . . . . . . 17 1 1 1c Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
37 df-rex 2620 . . . . . . . . . . . . . . . . 17 1 1 1c Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk 1 1 1c Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
38 excom 1741 . . . . . . . . . . . . . . . . 17 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
3936, 37, 383bitr4i 268 . . . . . . . . . . . . . . . 16 1 1 1c Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
40 snex 4111 . . . . . . . . . . . . . . . . . . 19
41 opkeq1 4059 . . . . . . . . . . . . . . . . . . . 20
4241eleq1d 2419 . . . . . . . . . . . . . . . . . . 19 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
4340, 42ceqsexv 2894 . . . . . . . . . . . . . . . . . 18 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
44 elin 3219 . . . . . . . . . . . . . . . . . 18 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
45 snex 4111 . . . . . . . . . . . . . . . . . . . . 21
4645, 11, 1otkelins3k 4256 . . . . . . . . . . . . . . . . . . . 20 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c
47 vex 2862 . . . . . . . . . . . . . . . . . . . . 21
48 snex 4111 . . . . . . . . . . . . . . . . . . . . 21
4947, 48opksnelsik 4265 . . . . . . . . . . . . . . . . . . . 20 SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c
50 vex 2862 . . . . . . . . . . . . . . . . . . . . 21
5147, 50eqpw1relk 4479 . . . . . . . . . . . . . . . . . . . 20 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c 1
5246, 49, 513bitri 262 . . . . . . . . . . . . . . . . . . 19 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c 1
5345, 11, 1otkelins2k 4255 . . . . . . . . . . . . . . . . . . . 20 Ins2k Sk Sk
5447, 1elssetk 4270 . . . . . . . . . . . . . . . . . . . 20 Sk
5553, 54bitri 240 . . . . . . . . . . . . . . . . . . 19 Ins2k Sk
5652, 55anbi12i 678 . . . . . . . . . . . . . . . . . 18 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk 1
5743, 44, 563bitri 262 . . . . . . . . . . . . . . . . 17 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk 1
5857exbii 1582 . . . . . . . . . . . . . . . 16 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk 1
5931, 39, 583bitri 262 . . . . . . . . . . . . . . 15 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c 1
6025, 15opkelxpk 4248 . . . . . . . . . . . . . . . 16 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c
6125, 60mpbiran 884 . . . . . . . . . . . . . . 15 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c
62 df-clel 2349 . . . . . . . . . . . . . . 15 1 1
6359, 61, 623bitr4i 268 . . . . . . . . . . . . . 14 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c 1
64 opkex 4113 . . . . . . . . . . . . . . . . 17
6564elimak 4259 . . . . . . . . . . . . . . . 16 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c 1 1 1c Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
6632anbi1i 676 . . . . . . . . . . . . . . . . . . 19 1 1 1c Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
67 19.41v 1901 . . . . . . . . . . . . . . . . . . 19 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
6866, 67bitr4i 243 . . . . . . . . . . . . . . . . . 18 1 1 1c Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
6968exbii 1582 . . . . . . . . . . . . . . . . 17 1 1 1c Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
70 df-rex 2620 . . . . . . . . . . . . . . . . 17 1 1 1c Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk 1 1 1c Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
71 excom 1741 . . . . . . . . . . . . . . . . 17 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
7269, 70, 713bitr4i 268 . . . . . . . . . . . . . . . 16 1 1 1c Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
73 opkeq1 4059 . . . . . . . . . . . . . . . . . . . 20
7473eleq1d 2419 . . . . . . . . . . . . . . . . . . 19 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
7540, 74ceqsexv 2894 . . . . . . . . . . . . . . . . . 18 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
76 elin 3219 . . . . . . . . . . . . . . . . . 18 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
77 snex 4111 . . . . . . . . . . . . . . . . . . . . 21
7845, 77, 1otkelins3k 4256 . . . . . . . . . . . . . . . . . . . 20 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c
79 snex 4111 . . . . . . . . . . . . . . . . . . . . 21
8047, 79opksnelsik 4265 . . . . . . . . . . . . . . . . . . . 20 SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c
81 vex 2862 . . . . . . . . . . . . . . . . . . . . 21
8247, 81eqpw1relk 4479 . . . . . . . . . . . . . . . . . . . 20 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c 1
8378, 80, 823bitri 262 . . . . . . . . . . . . . . . . . . 19 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c 1
8445, 77, 1otkelins2k 4255 . . . . . . . . . . . . . . . . . . . 20 Ins2k Sk Sk
8584, 54bitri 240 . . . . . . . . . . . . . . . . . . 19 Ins2k Sk
8683, 85anbi12i 678 . . . . . . . . . . . . . . . . . 18 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk 1
8775, 76, 863bitri 262 . . . . . . . . . . . . . . . . 17 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk 1
8887exbii 1582 . . . . . . . . . . . . . . . 16 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk 1
8965, 72, 883bitri 262 . . . . . . . . . . . . . . 15 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c 1
9077, 11, 1otkelins2k 4255 . . . . . . . . . . . . . . 15 Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c
91 df-clel 2349 . . . . . . . . . . . . . . 15 1 1
9289, 90, 913bitr4i 268 . . . . . . . . . . . . . 14 Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c 1
9363, 92anbi12i 678 . . . . . . . . . . . . 13 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c 1 1
9430, 93bitri 240 . . . . . . . . . . . 12 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c 1 1
9577, 11, 1otkelins3k 4256 . . . . . . . . . . . . . 14 Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn SIk Ins2k k Sk Ins3k k Sk k1 1 Nn
9679, 48opksnelsik 4265 . . . . . . . . . . . . . 14 SIk Ins2k k Sk Ins3k k Sk k1 1 Nn Ins2k k Sk Ins3k k Sk k1 1 Nn
97 opkex 4113 . . . . . . . . . . . . . . . 16
9897elimak 4259 . . . . . . . . . . . . . . 15 Ins2k k Sk Ins3k k Sk k1 1 Nn 1 1 Nn Ins2k k Sk Ins3k k Sk
99 elpw12 4145 . . . . . . . . . . . . . . . . . . 19 1 1 Nn Nn
10099anbi1i 676 . . . . . . . . . . . . . . . . . 18 1 1 Nn Ins2k k Sk Ins3k k Sk Nn Ins2k k Sk Ins3k k Sk
101 r19.41v 2764 . . . . . . . . . . . . . . . . . 18 Nn Ins2k k Sk Ins3k k Sk Nn Ins2k k Sk Ins3k k Sk
102100, 101bitr4i 243 . . . . . . . . . . . . . . . . 17 1 1 Nn Ins2k k Sk Ins3k k Sk Nn Ins2k k Sk Ins3k k Sk
103102exbii 1582 . . . . . . . . . . . . . . . 16 1 1 Nn Ins2k k Sk Ins3k k Sk Nn Ins2k k Sk Ins3k k Sk
104 df-rex 2620 . . . . . . . . . . . . . . . 16 1 1 Nn Ins2k k Sk Ins3k k Sk 1 1 Nn Ins2k k Sk Ins3k k Sk
105 rexcom4 2878 . . . . . . . . . . . . . . . 16 Nn Ins2k k Sk Ins3k k Sk Nn Ins2k k Sk Ins3k k Sk
106103, 104, 1053bitr4i 268 . . . . . . . . . . . . . . 15 1 1 Nn Ins2k k Sk Ins3k k Sk Nn Ins2k k Sk Ins3k k Sk
107 snex 4111 . . . . . . . . . . . . . . . . . 18
108 opkeq1 4059 . . . . . . . . . . . . . . . . . . 19
109108eleq1d 2419 . . . . . . . . . . . . . . . . . 18 Ins2k k Sk Ins3k k Sk Ins2k k Sk Ins3k k Sk
110107, 109ceqsexv 2894 . . . . . . . . . . . . . . . . 17 Ins2k k Sk Ins3k k Sk Ins2k k Sk Ins3k k Sk
111 elin 3219 . . . . . . . . . . . . . . . . 17 Ins2k k Sk Ins3k k Sk Ins2k k Sk Ins3k k Sk
112 vex 2862 . . . . . . . . . . . . . . . . . . . 20
113112, 79, 48otkelins2k 4255 . . . . . . . . . . . . . . . . . . 19 Ins2k k Sk k Sk
114112, 48opkelcnvk 4250 . . . . . . . . . . . . . . . . . . 19 k Sk Sk
11550, 112elssetk 4270 . . . . . . . . . . . . . . . . . . 19 Sk
116113, 114, 1153bitri 262 . . . . . . . . . . . . . . . . . 18 Ins2k k Sk
117112, 79, 48otkelins3k 4256 . . . . . . . . . . . . . . . . . . 19 Ins3k k Sk k Sk
118112, 79opkelcnvk 4250 . . . . . . . . . . . . . . . . . . 19 k Sk Sk
11981, 112elssetk 4270 . . . . . . . . . . . . . . . . . . 19 Sk
120117, 118, 1193bitri 262 . . . . . . . . . . . . . . . . . 18 Ins3k k Sk
121116, 120anbi12i 678 . . . . . . . . . . . . . . . . 17 Ins2k k Sk Ins3k k Sk
122110, 111, 1213bitri 262 . . . . . . . . . . . . . . . 16 Ins2k k Sk Ins3k k Sk
123122rexbii 2639 . . . . . . . . . . . . . . 15 Nn Ins2k k Sk Ins3k k Sk Nn
12498, 106, 1233bitri 262 . . . . . . . . . . . . . 14 Ins2k k Sk Ins3k k Sk k1 1 Nn Nn
12595, 96, 1243bitri 262 . . . . . . . . . . . . 13 Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn Nn
126125notbii 287 . . . . . . . . . . . 12 Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn Nn
12794, 126anbi12i 678 . . . . . . . . . . 11 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn 1 1 Nn
12828, 29, 1273bitri 262 . . . . . . . . . 10 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn 1 1 Nn
129128exbii 1582 . . . . . . . . 9 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn 1 1 Nn
13016, 24, 1293bitri 262 . . . . . . . 8 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c 1 1 Nn
131 exanali 1585 . . . . . . . 8 1 1 Nn 1 1 Nn
13214, 130, 1313bitri 262 . . . . . . 7 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c 1 1 Nn
133132exbii 1582 . . . . . 6 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c 1 1 Nn
1342, 10, 1333bitri 262 . . . . 5 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1ck1 1c 1 1 Nn
135134notbii 287 . . . 4 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1ck1 1c 1 1 Nn
1361elcompl 3225 . . . 4 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1ck1 1c k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1ck1 1c
137 alex 1572 . . . 4 1 1 Nn 1 1 Nn
138135, 136, 1373bitr4i 268 . . 3 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1ck1 1c 1 1 Nn
139138abbi2i 2464 . 2 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1ck1 1c 1 1 Nn
140 vvex 4109 . . . . . . . 8
141 1cex 4142 . . . . . . . . . . . . . . 15 1c
142141pwex 4329 . . . . . . . . . . . . . 14 1c
143142, 140xpkex 4289 . . . . . . . . . . . . 13 1c k
144 ssetkex 4294 . . . . . . . . . . . . . . . 16 Sk
145144ins3kex 4308 . . . . . . . . . . . . . . 15 Ins3k Sk
146144sikex 4297 . . . . . . . . . . . . . . . 16 SIk Sk
147146ins2kex 4307 . . . . . . . . . . . . . . 15 Ins2k SIk Sk
148145, 147symdifex 4108 . . . . . . . . . . . . . 14 Ins3k Sk Ins2k SIk Sk
149141pw1ex 4303 . . . . . . . . . . . . . . . 16 1 1c
150149pw1ex 4303 . . . . . . . . . . . . . . 15 1 1 1c
151150pw1ex 4303 . . . . . . . . . . . . . 14 1 1 1 1c
152148, 151imakex 4300 . . . . . . . . . . . . 13 Ins3k Sk Ins2k SIk Sk k1 1 1 1c
153143, 152difex 4107 . . . . . . . . . . . 12 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c
154153sikex 4297 . . . . . . . . . . 11 SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c
155154ins3kex 4308 . . . . . . . . . 10 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c
156144ins2kex 4307 . . . . . . . . . 10 Ins2k Sk
157155, 156inex 4105 . . . . . . . . 9 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk
158157, 150imakex 4300 . . . . . . . 8 Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c
159140, 158xpkex 4289 . . . . . . 7 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c
160158ins2kex 4307 . . . . . . 7 Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c
161159, 160inex 4105 . . . . . 6 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c
162144cnvkex 4287 . . . . . . . . . . 11 k Sk
163162ins2kex 4307 . . . . . . . . . 10 Ins2k k Sk
164162ins3kex 4308 . . . . . . . . . 10 Ins3k k Sk
165163, 164inex 4105 . . . . . . . . 9 Ins2k k Sk Ins3k k Sk
166 nncex 4396 . . . . . . . . . . 11 Nn
167166pw1ex 4303 . . . . . . . . . 10 1 Nn
168167pw1ex 4303 . . . . . . . . 9 1 1 Nn
169165, 168imakex 4300 . . . . . . . 8 Ins2k k Sk Ins3k k Sk k1 1 Nn
170169sikex 4297 . . . . . . 7 SIk Ins2k k Sk Ins3k k Sk k1 1 Nn
171170ins3kex 4308 . . . . . 6 Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn
172161, 171difex 4107 . . . . 5 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn
173172, 151imakex 4300 . . . 4 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1c
174173, 149imakex 4300 . . 3 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1ck1 1c
175174complex 4104 . 2 k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins3k SIk Ins2k k Sk Ins3k k Sk k1 1 Nn k1 1 1 1ck1 1c
176139, 175eqeltrri 2424 1 1 1 Nn
Colors of variables: wff setvar class
Syntax hints:   wn 3   wi 4   wa 358  wal 1540  wex 1541   wceq 1642   wcel 1710  cab 2339  wrex 2615  cvv 2859   ∼ ccompl 3205   cdif 3206   cin 3208   csymdif 3209  cpw 3722  csn 3737  copk 4057  1cc1c 4134  1 cpw1 4135   k cxpk 4174  kccnvk 4175   Ins2k cins2k 4176   Ins3k cins3k 4177  kcimak 4179   SIk csik 4181   Sk cssetk 4183   Nn cnnc 4373
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
This theorem is referenced by:  ncfinlower  4483
  Copyright terms: Public domain W3C validator