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

Theorem ncfinraiselem2 4480
Description: Lemma for ncfinraise 4481. Show stratification for induction. (Contributed by SF, 22-Jan-2015.)
Assertion
Ref Expression
ncfinraiselem2 Nn 1 1
Distinct variable groups:   ,,   ,   ,   ,

Proof of Theorem ncfinraiselem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snex 4111 . . . . . 6
21elcompl 3225 . . . . 5 SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1ck1 1c SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1ck1 1c
31elimak 4259 . . . . . 6 SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1ck1 1c 1 1c SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c
4 elpw11c 4147 . . . . . . . . . 10 1 1c
54anbi1i 676 . . . . . . . . 9 1 1c SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c
6 19.41v 1901 . . . . . . . . 9 SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c
75, 6bitr4i 243 . . . . . . . 8 1 1c SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c
87exbii 1582 . . . . . . 7 1 1c SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c
9 df-rex 2620 . . . . . . 7 1 1c SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c 1 1c SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c
10 excom 1741 . . . . . . 7 SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c
118, 9, 103bitr4i 268 . . . . . 6 1 1c SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c
12 snex 4111 . . . . . . . . . 10
13 opkeq1 4059 . . . . . . . . . . 11
1413eleq1d 2419 . . . . . . . . . 10 SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c
1512, 14ceqsexv 2894 . . . . . . . . 9 SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c
16 elin 3219 . . . . . . . . 9 SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c
17 snex 4111 . . . . . . . . . . . 12
18 vex 2862 . . . . . . . . . . . 12
1917, 18opksnelsik 4265 . . . . . . . . . . 11 SIk Sk Sk
20 vex 2862 . . . . . . . . . . . 12
2120, 18elssetk 4270 . . . . . . . . . . 11 Sk
2219, 21bitri 240 . . . . . . . . . 10 SIk Sk
23 opkex 4113 . . . . . . . . . . . . 13
2423elimak 4259 . . . . . . . . . . . 12 Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c 1 1 1 1c Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c
25 df-rex 2620 . . . . . . . . . . . 12 1 1 1 1c Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c 1 1 1 1c Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c
26 elpw131c 4149 . . . . . . . . . . . . . . . 16 1 1 1 1c
2726anbi1i 676 . . . . . . . . . . . . . . 15 1 1 1 1c Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c
28 19.41v 1901 . . . . . . . . . . . . . . 15 Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c
2927, 28bitr4i 243 . . . . . . . . . . . . . 14 1 1 1 1c Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c
3029exbii 1582 . . . . . . . . . . . . 13 1 1 1 1c Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c
31 excom 1741 . . . . . . . . . . . . 13 Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c
3230, 31bitr4i 243 . . . . . . . . . . . 12 1 1 1 1c Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c
3324, 25, 323bitri 262 . . . . . . . . . . 11 Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c
34 snex 4111 . . . . . . . . . . . . . . 15
35 opkeq1 4059 . . . . . . . . . . . . . . . 16
3635eleq1d 2419 . . . . . . . . . . . . . . 15 Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c
3734, 36ceqsexv 2894 . . . . . . . . . . . . . 14 Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c
38 eldif 3221 . . . . . . . . . . . . . 14 Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c
39 snex 4111 . . . . . . . . . . . . . . . . 17
4039, 12, 1otkelins2k 4255 . . . . . . . . . . . . . . . 16 Ins2k SIk Sk SIk Sk
41 snex 4111 . . . . . . . . . . . . . . . . 17
4241, 18opksnelsik 4265 . . . . . . . . . . . . . . . 16 SIk Sk Sk
43 vex 2862 . . . . . . . . . . . . . . . . 17
4443, 18elssetk 4270 . . . . . . . . . . . . . . . 16 Sk
4540, 42, 443bitri 262 . . . . . . . . . . . . . . 15 Ins2k SIk Sk
4639, 12, 1otkelins3k 4256 . . . . . . . . . . . . . . . . 17 Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c
47 df-rex 2620 . . . . . . . . . . . . . . . . . . 19 1 1c 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c 1 1c 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c
48 elpw11c 4147 . . . . . . . . . . . . . . . . . . . . . 22 1 1c
4948anbi1i 676 . . . . . . . . . . . . . . . . . . . . 21 1 1c 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c
50 19.41v 1901 . . . . . . . . . . . . . . . . . . . . 21 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c
5149, 50bitr4i 243 . . . . . . . . . . . . . . . . . . . 20 1 1c 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c
5251exbii 1582 . . . . . . . . . . . . . . . . . . 19 1 1c 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c
5347, 52bitri 240 . . . . . . . . . . . . . . . . . 18 1 1c 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c
54 opkex 4113 . . . . . . . . . . . . . . . . . . 19
5554elimak 4259 . . . . . . . . . . . . . . . . . 18 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c 1 1c 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c
56 excom 1741 . . . . . . . . . . . . . . . . . 18 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c
5753, 55, 563bitr4i 268 . . . . . . . . . . . . . . . . 17 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c
58 snex 4111 . . . . . . . . . . . . . . . . . . . . 21
59 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . 22
6059eleq1d 2419 . . . . . . . . . . . . . . . . . . . . 21 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c
6158, 60ceqsexv 2894 . . . . . . . . . . . . . . . . . . . 20 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c
62 elin 3219 . . . . . . . . . . . . . . . . . . . 20 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c
6358, 54opkelxpk 4248 . . . . . . . . . . . . . . . . . . . . . . 23 1 1 Nn k 1 1 Nn
6454, 63mpbiran2 885 . . . . . . . . . . . . . . . . . . . . . 22 1 1 Nn k 1 1 Nn
65 snelpw1 4146 . . . . . . . . . . . . . . . . . . . . . 22 1 1 Nn 1 Nn
66 snelpw1 4146 . . . . . . . . . . . . . . . . . . . . . 22 1 Nn Nn
6764, 65, 663bitri 262 . . . . . . . . . . . . . . . . . . . . 21 1 1 Nn k Nn
68 elin 3219 . . . . . . . . . . . . . . . . . . . . . 22 Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c
69 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . 25
7069, 39, 12otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c
71 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7271elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c 1 1 1c Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
73 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 1 1c Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk 1 1 1c Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
74 elpw121c 4148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 1 1c
7574anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 1 1c Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
76 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
7775, 76bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1 1 1c Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
7877exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 1 1c Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
79 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
8078, 79bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 1 1c Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
8172, 73, 803bitri 262 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
82 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
83 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8483eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
8582, 84ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
86 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
87 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
8887, 69, 12otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c
89 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
9089, 17opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c
9189, 20eqpw1relk 4479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c 1
9288, 90, 913bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c 1
9387, 69, 12otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins3k Sk Sk
9489, 69elssetk 4270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Sk
9593, 94bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins3k Sk
9692, 95anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk 1
9785, 86, 963bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk 1
9897exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk 1
99 df-clel 2349 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 1
10098, 99bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk 1
10170, 81, 1003bitri 262 . . . . . . . . . . . . . . . . . . . . . . 23 Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c 1
102 opkex 4113 . . . . . . . . . . . . . . . . . . . . . . . . . 26
103102elimak 4259 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c 1 1 1c Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
10474anbi1i 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 1 1c Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
105 19.41v 1901 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
106104, 105bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1 1 1c Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
107106exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 1 1c Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
108 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 1 1c Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk 1 1 1c Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
109 excom 1741 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
110107, 108, 1093bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 1 1c Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
111 opkeq1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
112111eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
11382, 112ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
114 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
11587, 69, 39otkelins2k 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c
11689, 41opksnelsik 4265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c
11789, 43eqpw1relk 4479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c 1
118115, 116, 1173bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c 1
11987, 69, 39otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Ins3k Sk Sk
120119, 94bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ins3k Sk
121118, 120anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk 1
122113, 114, 1213bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk 1
123122exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk 1
124103, 110, 1233bitri 262 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c 1
12569, 39, 12otkelins3k 4256 . . . . . . . . . . . . . . . . . . . . . . . 24 Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c
126 df-clel 2349 . . . . . . . . . . . . . . . . . . . . . . . 24 1 1
127124, 125, 1263bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . 23 Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c 1
128101, 127anbi12i 678 . . . . . . . . . . . . . . . . . . . . . 22 Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c 1 1
12968, 128bitri 240 . . . . . . . . . . . . . . . . . . . . 21 Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c 1 1
13067, 129anbi12i 678 . . . . . . . . . . . . . . . . . . . 20 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Nn 1 1
13161, 62, 1303bitri 262 . . . . . . . . . . . . . . . . . . 19 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Nn 1 1
132131exbii 1582 . . . . . . . . . . . . . . . . . 18 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Nn 1 1
133 df-rex 2620 . . . . . . . . . . . . . . . . . 18 Nn 1 1 Nn 1 1
134132, 133bitr4i 243 . . . . . . . . . . . . . . . . 17 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Nn 1 1
13546, 57, 1343bitri 262 . . . . . . . . . . . . . . . 16 Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c Nn 1 1
136135notbii 287 . . . . . . . . . . . . . . 15 Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c Nn 1 1
13745, 136anbi12i 678 . . . . . . . . . . . . . 14 Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c Nn 1 1
13837, 38, 1373bitri 262 . . . . . . . . . . . . 13 Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c Nn 1 1
139138exbii 1582 . . . . . . . . . . . 12 Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c Nn 1 1
140 df-rex 2620 . . . . . . . . . . . 12 Nn 1 1 Nn 1 1
141139, 140bitr4i 243 . . . . . . . . . . 11 Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c Nn 1 1
142 rexnal 2625 . . . . . . . . . . 11 Nn 1 1 Nn 1 1
14333, 141, 1423bitri 262 . . . . . . . . . 10 Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c Nn 1 1
14422, 143anbi12i 678 . . . . . . . . 9 SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c Nn 1 1
14515, 16, 1443bitri 262 . . . . . . . 8 SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c Nn 1 1
146145exbii 1582 . . . . . . 7 SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c Nn 1 1
147 df-rex 2620 . . . . . . 7 Nn 1 1 Nn 1 1
148146, 147bitr4i 243 . . . . . 6 SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c Nn 1 1
1493, 11, 1483bitri 262 . . . . 5 SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1ck1 1c Nn 1 1
1502, 149xchbinx 301 . . . 4 SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1ck1 1c Nn 1 1
15118eluni1 4173 . . . 4 1 SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1ck1 1c SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1ck1 1c
152 dfral2 2626 . . . 4 Nn 1 1 Nn 1 1
153150, 151, 1523bitr4i 268 . . 3 1 SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1ck1 1c Nn 1 1
154153abbi2i 2464 . 2 1 SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1ck1 1c Nn 1 1
155 ssetkex 4294 . . . . . . 7 Sk
156155sikex 4297 . . . . . 6 SIk Sk
157156ins2kex 4307 . . . . . . . 8 Ins2k SIk Sk
158 nncex 4396 . . . . . . . . . . . . . 14 Nn
159158pw1ex 4303 . . . . . . . . . . . . 13 1 Nn
160159pw1ex 4303 . . . . . . . . . . . 12 1 1 Nn
161 vvex 4109 . . . . . . . . . . . 12
162160, 161xpkex 4289 . . . . . . . . . . 11 1 1 Nn k
163 1cex 4142 . . . . . . . . . . . . . . . . . . . 20 1c
164163pwex 4329 . . . . . . . . . . . . . . . . . . 19 1c
165164, 161xpkex 4289 . . . . . . . . . . . . . . . . . 18 1c k
166155ins3kex 4308 . . . . . . . . . . . . . . . . . . . 20 Ins3k Sk
167166, 157symdifex 4108 . . . . . . . . . . . . . . . . . . 19 Ins3k Sk Ins2k SIk Sk
168163pw1ex 4303 . . . . . . . . . . . . . . . . . . . . 21 1 1c
169168pw1ex 4303 . . . . . . . . . . . . . . . . . . . 20 1 1 1c
170169pw1ex 4303 . . . . . . . . . . . . . . . . . . 19 1 1 1 1c
171167, 170imakex 4300 . . . . . . . . . . . . . . . . . 18 Ins3k Sk Ins2k SIk Sk k1 1 1 1c
172165, 171difex 4107 . . . . . . . . . . . . . . . . 17 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c
173172sikex 4297 . . . . . . . . . . . . . . . 16 SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c
174173ins2kex 4307 . . . . . . . . . . . . . . 15 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c
175174, 166inex 4105 . . . . . . . . . . . . . 14 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk
176175, 169imakex 4300 . . . . . . . . . . . . 13 Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c
177176ins2kex 4307 . . . . . . . . . . . 12 Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c
178176ins3kex 4308 . . . . . . . . . . . 12 Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c
179177, 178inex 4105 . . . . . . . . . . 11 Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c
180162, 179inex 4105 . . . . . . . . . 10 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c
181180, 168imakex 4300 . . . . . . . . 9 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c
182181ins3kex 4308 . . . . . . . 8 Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c
183157, 182difex 4107 . . . . . . 7 Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1c
184183, 170imakex 4300 . . . . . 6 Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c
185156, 184inex 4105 . . . . 5 SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1c
186185, 168imakex 4300 . . . 4 SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1ck1 1c
187186complex 4104 . . 3 SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1ck1 1c
188187uni1ex 4293 . 2 1 SIk Sk Ins2k SIk Sk Ins3k 1 1 Nn k Ins2k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1c Ins3k Ins2k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk k1 1 1ck1 1ck1 1 1 1ck1 1c
189154, 188eqeltrri 2424 1 Nn 1 1
Colors of variables: wff setvar class
Syntax hints:   wn 3   wa 358  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  copk 4057  ⋃1cuni1 4133  1cc1c 4134  1 cpw1 4135   k cxpk 4174   Ins2k cins2k 4176   Ins3k cins3k 4177  kcimak 4179   SIk csik 4181   Sk cssetk 4183   Nn cnnc 4373
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
This theorem is referenced by:  ncfinraise  4481
  Copyright terms: Public domain W3C validator