Step | Hyp | Ref
| Expression |
1 | | tfineq 4488 |
. . . . . . . . . . 11
![(](lp.gif) Tfin
Tfin ![n](_n.gif) ![)](rp.gif) |
2 | 1 | eqeq2d 2364 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif)
Tfin Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
3 | 2 | cbvrexv 2836 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif)
Spfin Tfin ![E.](exists.gif)
Spfin
Tfin ![n](_n.gif) ![)](rp.gif) |
4 | | vfinspsslem1 4550 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Tfin Spfin ![(](lp.gif)
Spfin Sfin ![(](lp.gif) ![z](_z.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif)
Spfin Tfin ![x](_x.gif) ![)](rp.gif) |
5 | 4 | expr 598 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Tfin Spfin
Spfin Sfin ![(](lp.gif) ![z](_z.gif)
Tfin ![n](_n.gif) ![E.](exists.gif) Spfin Tfin
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
6 | | eleq1 2413 |
. . . . . . . . . . . . . . 15
![(](lp.gif) Tfin ![(](lp.gif) Spfin Tfin
Spfin ![)](rp.gif) ![)](rp.gif) |
7 | 6 | anbi2d 684 |
. . . . . . . . . . . . . 14
![(](lp.gif) Tfin ![(](lp.gif) ![(](lp.gif) Fin Spfin ![(](lp.gif) Fin Tfin
Spfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
8 | 7 | anbi1d 685 |
. . . . . . . . . . . . 13
![(](lp.gif) Tfin ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Spfin Spfin ![(](lp.gif) ![(](lp.gif) Fin Tfin
Spfin
Spfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
9 | | sfineq2 4527 |
. . . . . . . . . . . . . 14
![(](lp.gif) Tfin Sfin ![(](lp.gif) ![z](_z.gif)
![w](_w.gif) Sfin ![(](lp.gif) ![z](_z.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
10 | 9 | imbi1d 308 |
. . . . . . . . . . . . 13
![(](lp.gif) Tfin ![(](lp.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![w](_w.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) Sfin ![(](lp.gif) ![z](_z.gif) Tfin ![n](_n.gif)
![E.](exists.gif) Spfin Tfin
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
11 | 8, 10 | imbi12d 311 |
. . . . . . . . . . . 12
![(](lp.gif) Tfin ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Spfin Spfin Sfin ![(](lp.gif) ![z](_z.gif) ![w](_w.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Tfin Spfin
Spfin Sfin ![(](lp.gif) ![z](_z.gif)
Tfin ![n](_n.gif) ![E.](exists.gif) Spfin Tfin
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
12 | 5, 11 | mpbiri 224 |
. . . . . . . . . . 11
![(](lp.gif) Tfin ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Spfin Spfin Sfin ![(](lp.gif) ![z](_z.gif) ![w](_w.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | 12 | com12 27 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Spfin Spfin ![(](lp.gif) Tfin
Sfin ![(](lp.gif) ![z](_z.gif) ![w](_w.gif) ![E.](exists.gif)
Spfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
14 | 13 | rexlimdva 2738 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Fin Spfin ![(](lp.gif) ![E.](exists.gif) Spfin Tfin
Sfin ![(](lp.gif) ![z](_z.gif) ![w](_w.gif) ![E.](exists.gif)
Spfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
15 | 3, 14 | syl5bi 208 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Fin Spfin ![(](lp.gif) ![E.](exists.gif) Spfin Tfin
Sfin ![(](lp.gif) ![z](_z.gif) ![w](_w.gif) ![E.](exists.gif)
Spfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
16 | | sfineq2 4527 |
. . . . . . . . . . . 12
![(](lp.gif) Ncfin Sfin ![(](lp.gif) ![z](_z.gif)
![w](_w.gif) Sfin ![(](lp.gif) ![z](_z.gif) Ncfin ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 16 | biimpa 470 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) Ncfin Sfin ![(](lp.gif) ![z](_z.gif)
![w](_w.gif) ![)](rp.gif) Sfin ![(](lp.gif) ![z](_z.gif)
Ncfin ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
18 | | 1cvsfin 4542 |
. . . . . . . . . . . 12
![(](lp.gif) Fin Sfin
Ncfin 1c Ncfin ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
19 | | sfin111 4536 |
. . . . . . . . . . . . 13
![(](lp.gif) Sfin
Ncfin 1c Ncfin ![_V](rmcv.gif)
Sfin ![(](lp.gif) ![z](_z.gif) Ncfin ![_V](rmcv.gif) ![)](rp.gif) Ncfin 1c ![z](_z.gif) ![)](rp.gif) |
20 | | tncveqnc1fin 4544 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) Fin Tfin
Ncfin Ncfin
1c![)](rp.gif) |
21 | 20 | eqcomd 2358 |
. . . . . . . . . . . . . . 15
![(](lp.gif) Fin Ncfin 1c Tfin Ncfin ![_V](rmcv.gif) ![)](rp.gif) |
22 | | ncvspfin 4538 |
. . . . . . . . . . . . . . . 16
Ncfin Spfin |
23 | | tfineq 4488 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) Ncfin Tfin Tfin
Ncfin ![_V](rmcv.gif) ![)](rp.gif) |
24 | 23 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) Ncfin Ncfin 1c
Tfin Ncfin
1c
Tfin Ncfin ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 24 | rspcev 2955 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) Ncfin
Spfin Ncfin
1c
Tfin Ncfin ![_V](rmcv.gif)
![E.](exists.gif) Spfin Ncfin 1c Tfin ![x](_x.gif) ![)](rp.gif) |
26 | 22, 25 | mpan 651 |
. . . . . . . . . . . . . . 15
Ncfin 1c Tfin Ncfin ![E.](exists.gif) Spfin
Ncfin 1c Tfin ![x](_x.gif) ![)](rp.gif) |
27 | 21, 26 | syl 15 |
. . . . . . . . . . . . . 14
![(](lp.gif) Fin ![E.](exists.gif)
Spfin Ncfin 1c Tfin ![x](_x.gif) ![)](rp.gif) |
28 | | eqeq1 2359 |
. . . . . . . . . . . . . . . . 17
Ncfin 1c Ncfin 1c Tfin Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 28 | rexbidv 2635 |
. . . . . . . . . . . . . . . 16
Ncfin 1c ![(](lp.gif) ![E.](exists.gif) Spfin Ncfin 1c Tfin ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
30 | 29 | biimpd 198 |
. . . . . . . . . . . . . . 15
Ncfin 1c ![(](lp.gif) ![E.](exists.gif) Spfin Ncfin 1c Tfin ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
31 | 30 | com12 27 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![E.](exists.gif)
Spfin Ncfin 1c Tfin Ncfin 1c ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
32 | 27, 31 | syl 15 |
. . . . . . . . . . . . 13
![(](lp.gif) Fin Ncfin
1c
![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
33 | 19, 32 | syl5 28 |
. . . . . . . . . . . 12
![(](lp.gif) Fin ![(](lp.gif)
Sfin Ncfin
1c
Ncfin ![_V](rmcv.gif) Sfin ![(](lp.gif) ![z](_z.gif) Ncfin ![_V](rmcv.gif) ![)](rp.gif) ![E.](exists.gif)
Spfin Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
34 | 18, 33 | mpand 656 |
. . . . . . . . . . 11
![(](lp.gif) Fin Sfin ![(](lp.gif) ![z](_z.gif) Ncfin ![_V](rmcv.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 17, 34 | syl5 28 |
. . . . . . . . . 10
![(](lp.gif) Fin ![(](lp.gif) ![(](lp.gif) Ncfin Sfin ![(](lp.gif) ![z](_z.gif)
![w](_w.gif) ![)](rp.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 35 | exp3a 425 |
. . . . . . . . 9
![(](lp.gif) Fin ![(](lp.gif)
Ncfin Sfin ![(](lp.gif) ![z](_z.gif) ![w](_w.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 36 | adantr 451 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Fin Spfin ![(](lp.gif) Ncfin
Sfin ![(](lp.gif) ![z](_z.gif) ![w](_w.gif) ![E.](exists.gif)
Spfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
38 | 15, 37 | jaod 369 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Fin Spfin ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Spfin Tfin
Ncfin ![_V](rmcv.gif)
Sfin ![(](lp.gif) ![z](_z.gif) ![w](_w.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
39 | 38 | imp3a 420 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Fin Spfin ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Spfin
Tfin Ncfin ![_V](rmcv.gif)
Sfin ![(](lp.gif) ![z](_z.gif) ![w](_w.gif) ![)](rp.gif) ![E.](exists.gif) Spfin Tfin
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
40 | | elun 3220 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif)
Spfin
Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
41 | | vex 2862 |
. . . . . . . . . 10
![_V](rmcv.gif) |
42 | | eqeq1 2359 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif)
Tfin Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
43 | 42 | rexbidv 2635 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Spfin
Tfin ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
44 | 41, 43 | elab 2985 |
. . . . . . . . 9
![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif)
Spfin
Tfin ![x](_x.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![)](rp.gif) |
45 | 41 | elsnc 3756 |
. . . . . . . . 9
![(](lp.gif) Ncfin ![_V](rmcv.gif) Ncfin ![_V](rmcv.gif) ![)](rp.gif) |
46 | 44, 45 | orbi12i 507 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) ![(](lp.gif) ![E.](exists.gif) Spfin
Tfin Ncfin ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
47 | 40, 46 | bitri 240 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) ![(](lp.gif) ![E.](exists.gif)
Spfin Tfin
Ncfin ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
48 | 47 | anbi1i 676 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif)
![E.](exists.gif) Spfin Tfin
![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif)
Sfin ![(](lp.gif) ![z](_z.gif) ![w](_w.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Spfin Tfin
Ncfin ![_V](rmcv.gif)
Sfin ![(](lp.gif) ![z](_z.gif) ![w](_w.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
49 | | vex 2862 |
. . . . . . 7
![_V](rmcv.gif) |
50 | | eqeq1 2359 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
Tfin Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
51 | 50 | rexbidv 2635 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Spfin
Tfin ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
52 | 49, 51 | elab 2985 |
. . . . . 6
![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif)
Spfin
Tfin ![x](_x.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![)](rp.gif) |
53 | 39, 48, 52 | 3imtr4g 261 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Fin Spfin ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![w](_w.gif) ![)](rp.gif) ![{](lbrace.gif)
![E.](exists.gif) Spfin Tfin
![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
54 | | ssun1 3426 |
. . . . . 6
![{](lbrace.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif)
![(](lp.gif) ![{](lbrace.gif)
![E.](exists.gif) Spfin Tfin
![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) ![)](rp.gif) |
55 | 54 | sseli 3269 |
. . . . 5
![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif)
Spfin
Tfin ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif)
Spfin
Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
56 | 53, 55 | syl6 29 |
. . . 4
![(](lp.gif) ![(](lp.gif) Fin Spfin ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![w](_w.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif)
Spfin
Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
57 | 56 | alrimiv 1631 |
. . 3
![(](lp.gif) ![(](lp.gif) Fin Spfin ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif)
Spfin Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![w](_w.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif)
Spfin
Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
58 | 57 | ralrimiva 2697 |
. 2
![(](lp.gif) Fin ![A.](forall.gif)
Spfin ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![w](_w.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif)
Spfin
Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
59 | | vex 2862 |
. . . . . . . . 9
![_V](rmcv.gif) |
60 | 59 | elimak 4259 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 Spfin ![E.](exists.gif) 1 Spfin ![<<](llangle.gif) ![t](_t.gif)
![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
61 | | df-rex 2620 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif)
1 Spfin ![<<](llangle.gif) ![t](_t.gif)
![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
1 Spfin ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
62 | | elpw1 4144 |
. . . . . . . . . . . . 13
![(](lp.gif) 1 Spfin ![E.](exists.gif) Spfin ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif) |
63 | 62 | anbi1i 676 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) 1 Spfin ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) Spfin
![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
64 | | r19.41v 2764 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif)
Spfin ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) Spfin
![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
65 | 63, 64 | bitr4i 243 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) 1 Spfin ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) Spfin ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
66 | 65 | exbii 1582 |
. . . . . . . . . 10
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 Spfin ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) Spfin ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
67 | | rexcom4 2878 |
. . . . . . . . . 10
![(](lp.gif) ![E.](exists.gif)
Spfin ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) Spfin ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
68 | 66, 67 | bitr4i 243 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 Spfin ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) Spfin ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
69 | 61, 68 | bitri 240 |
. . . . . . . 8
![(](lp.gif) ![E.](exists.gif)
1 Spfin ![<<](llangle.gif) ![t](_t.gif)
![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) Spfin ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
70 | 60, 69 | bitri 240 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 Spfin ![E.](exists.gif) Spfin ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
71 | | snex 4111 |
. . . . . . . . . 10
![{](lbrace.gif) ![x](_x.gif)
![_V](rmcv.gif) |
72 | | opkeq1 4059 |
. . . . . . . . . . 11
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![>>](rrangle.gif) ![)](rp.gif) |
73 | 72 | eleq1d 2419 |
. . . . . . . . . 10
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![(](lp.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
74 | 71, 73 | ceqsexv 2894 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
75 | | vex 2862 |
. . . . . . . . . 10
![_V](rmcv.gif) |
76 | 75, 59 | eqtfinrelk 4486 |
. . . . . . . . 9
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) Tfin
![x](_x.gif) ![)](rp.gif) |
77 | 74, 76 | bitri 240 |
. . . . . . . 8
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) Tfin ![x](_x.gif) ![)](rp.gif) |
78 | 77 | rexbii 2639 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif)
Spfin ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![<<](llangle.gif) ![t](_t.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![)](rp.gif) |
79 | 70, 78 | bitri 240 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 Spfin ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![)](rp.gif) |
80 | 79 | abbi2i 2464 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 Spfin
![{](lbrace.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![}](rbrace.gif) |
81 | | tfinrelkex 4487 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![_V](rmcv.gif) |
82 | | spfinex 4537 |
. . . . . . 7
Spfin ![_V](rmcv.gif) |
83 | 82 | pw1ex 4303 |
. . . . . 6
1 Spfin ![_V](rmcv.gif) |
84 | 81, 83 | imakex 4300 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ∼ ![(](lp.gif) Ins2k Sk Ins3k ![(](lp.gif) Ins3k k
Sk Ins2k ![(](lp.gif) Ins2k ![(](lp.gif) Nn k ![_V](rmcv.gif) ![(](lp.gif) Ins2k SIk Sk Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins3k k ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) k 1 Spfin
![_V](rmcv.gif) |
85 | 80, 84 | eqeltrri 2424 |
. . . 4
![{](lbrace.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![_V](rmcv.gif) |
86 | | snex 4111 |
. . . 4
Ncfin ![_V](rmcv.gif) ![_V](rmcv.gif) |
87 | 85, 86 | unex 4106 |
. . 3
![(](lp.gif) ![{](lbrace.gif)
![E.](exists.gif) Spfin Tfin
![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif)
![_V](rmcv.gif) |
88 | | ssun2 3427 |
. . . 4
Ncfin ![_V](rmcv.gif)
![(](lp.gif) ![{](lbrace.gif)
![E.](exists.gif) Spfin Tfin
![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) ![)](rp.gif) |
89 | | ncfinex 4472 |
. . . . 5
Ncfin ![_V](rmcv.gif) |
90 | 89 | snid 3760 |
. . . 4
Ncfin Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) |
91 | 88, 90 | sselii 3270 |
. . 3
Ncfin ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) ![)](rp.gif) |
92 | | spfininduct 4540 |
. . 3
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif)
Spfin
Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) Ncfin
![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif)
Spfin Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) ![A.](forall.gif)
Spfin ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![w](_w.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif)
Spfin
Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) Spfin ![(](lp.gif) ![{](lbrace.gif)
![E.](exists.gif) Spfin Tfin
![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
93 | 87, 91, 92 | mp3an12 1267 |
. 2
![(](lp.gif) ![A.](forall.gif)
Spfin ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) Sfin ![(](lp.gif) ![z](_z.gif) ![w](_w.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif)
Spfin
Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) ![)](rp.gif) Spfin ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif)
Spfin
Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
94 | 58, 93 | syl 15 |
1
![(](lp.gif) Fin Spfin ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif)
Spfin
Tfin ![x](_x.gif) Ncfin ![_V](rmcv.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |