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