Step | Hyp | Ref
| Expression |
1 | | simpl 443 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Fin Spfin Fin ![)](rp.gif) |
2 | | vfinspnn 4541 |
. . . . . . . 8
![(](lp.gif) Fin Spfin Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
3 | | difss 3393 |
. . . . . . . 8
Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) Nn |
4 | 2, 3 | syl6ss 3284 |
. . . . . . 7
![(](lp.gif) Fin Spfin Nn ![)](rp.gif) |
5 | 4 | sselda 3273 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Fin Spfin Nn ![)](rp.gif) |
6 | 2 | sselda 3273 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Fin Spfin Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
7 | | eldifsn 3839 |
. . . . . . . 8
![(](lp.gif) Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif)
Nn ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
8 | 7 | simprbi 450 |
. . . . . . 7
![(](lp.gif) Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
9 | 6, 8 | syl 15 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Fin Spfin ![(/)](varnothing.gif) ![)](rp.gif) |
10 | | vfintle 4546 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Fin Nn ![(/)](varnothing.gif) Tfin ![n](_n.gif) Ncfin 1c fin ![)](rp.gif) |
11 | 1, 5, 9, 10 | syl3anc 1182 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Fin Spfin
Tfin ![n](_n.gif) Ncfin
1c fin ![)](rp.gif) |
12 | 11 | ad2ant2r 727 |
. . . 4
![(](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) Tfin ![n](_n.gif)
Ncfin 1c fin ![)](rp.gif) |
13 | | t1csfin1c 4545 |
. . . . . . . 8
![(](lp.gif) Fin Sfin
Tfin Ncfin 1c Ncfin 1c![)](rp.gif) ![)](rp.gif) |
14 | 13 | adantr 451 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Fin Tfin Spfin Sfin
Tfin Ncfin 1c Ncfin 1c![)](rp.gif) ![)](rp.gif) |
15 | | simpr 447 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Spfin Sfin ![(](lp.gif) ![z](_z.gif) Tfin ![n](_n.gif) ![)](rp.gif)
Sfin ![(](lp.gif) ![z](_z.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
16 | | sfinltfin 4535 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Sfin Tfin Ncfin 1c Ncfin 1c Sfin ![(](lp.gif) ![z](_z.gif) Tfin ![n](_n.gif) ![)](rp.gif)
Tfin Ncfin 1c ![z](_z.gif) fin Ncfin 1c Tfin ![n](_n.gif) fin ![)](rp.gif) |
17 | 16 | ex 423 |
. . . . . . 7
![(](lp.gif) Sfin
Tfin Ncfin 1c Ncfin 1c Sfin ![(](lp.gif) ![z](_z.gif) Tfin ![n](_n.gif) ![)](rp.gif)
![(](lp.gif) Tfin Ncfin 1c ![z](_z.gif) fin
Ncfin 1c Tfin ![n](_n.gif) fin ![)](rp.gif) ![)](rp.gif) |
18 | 14, 15, 17 | syl2an 463 |
. . . . . 6
![(](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) ![(](lp.gif) Tfin Ncfin 1c ![z](_z.gif) fin
Ncfin 1c Tfin ![n](_n.gif) fin ![)](rp.gif) ![)](rp.gif) |
19 | 18 | con3d 125 |
. . . . 5
![(](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) ![(](lp.gif) Ncfin
1c
Tfin ![n](_n.gif) fin Tfin Ncfin 1c ![z](_z.gif) fin ![)](rp.gif) ![)](rp.gif) |
20 | 5 | ad2ant2r 727 |
. . . . . . 7
![(](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) Nn ![)](rp.gif) |
21 | | tfincl 4492 |
. . . . . . 7
![(](lp.gif) Nn Tfin Nn ![)](rp.gif) |
22 | 20, 21 | syl 15 |
. . . . . 6
![(](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) Tfin
Nn ![)](rp.gif) |
23 | | 1cex 4142 |
. . . . . . . . 9
1c
![_V](rmcv.gif) |
24 | | ncfinprop 4474 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Fin 1c ![_V](rmcv.gif) Ncfin
1c
Nn 1c Ncfin
1c![)](rp.gif) ![)](rp.gif) |
25 | 23, 24 | mpan2 652 |
. . . . . . . 8
![(](lp.gif) Fin Ncfin
1c
Nn 1c Ncfin
1c![)](rp.gif) ![)](rp.gif) |
26 | 25 | ad2antrr 706 |
. . . . . . 7
![(](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) Ncfin 1c Nn 1c
Ncfin 1c![)](rp.gif) ![)](rp.gif) |
27 | 26 | simpld 445 |
. . . . . 6
![(](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) Ncfin 1c Nn ![)](rp.gif) |
28 | | lenltfin 4469 |
. . . . . 6
![(](lp.gif) Tfin
Nn Ncfin 1c Nn ![(](lp.gif) Tfin ![n](_n.gif) Ncfin
1c fin Ncfin 1c Tfin ![n](_n.gif) fin ![)](rp.gif) ![)](rp.gif) |
29 | 22, 27, 28 | syl2anc 642 |
. . . . 5
![(](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) ![(](lp.gif) Tfin ![n](_n.gif) Ncfin 1c fin Ncfin 1c Tfin ![n](_n.gif) fin ![)](rp.gif) ![)](rp.gif) |
30 | | df-sfin 4446 |
. . . . . . . 8
Sfin ![(](lp.gif) ![z](_z.gif) Tfin ![n](_n.gif)
![(](lp.gif) Nn Tfin
Nn ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) 1
![~P](scrp.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
31 | 30 | simp1bi 970 |
. . . . . . 7
Sfin ![(](lp.gif) ![z](_z.gif) Tfin ![n](_n.gif)
Nn ![)](rp.gif) |
32 | 31 | ad2antll 709 |
. . . . . 6
![(](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) Nn ![)](rp.gif) |
33 | | tfincl 4492 |
. . . . . . 7
Ncfin 1c Nn Tfin Ncfin 1c Nn ![)](rp.gif) |
34 | 27, 33 | syl 15 |
. . . . . 6
![(](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) Tfin Ncfin 1c Nn ![)](rp.gif) |
35 | | lenltfin 4469 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Nn Tfin Ncfin 1c Nn ![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) Tfin Ncfin 1c fin Tfin Ncfin 1c ![z](_z.gif) fin ![)](rp.gif) ![)](rp.gif) |
36 | 32, 34, 35 | syl2anc 642 |
. . . . 5
![(](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) ![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) Tfin Ncfin 1c fin Tfin Ncfin 1c ![z](_z.gif) fin ![)](rp.gif) ![)](rp.gif) |
37 | 19, 29, 36 | 3imtr4d 259 |
. . . 4
![(](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) ![(](lp.gif) Tfin ![n](_n.gif) Ncfin 1c fin ![<<](llangle.gif) ![z](_z.gif)
Tfin Ncfin 1c fin ![)](rp.gif) ![)](rp.gif) |
38 | 12, 37 | mpd 14 |
. . 3
![(](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) ![<<](llangle.gif) ![z](_z.gif) Tfin Ncfin 1c fin ![)](rp.gif) |
39 | | vex 2862 |
. . . 4
![_V](rmcv.gif) |
40 | | tfinex 4485 |
. . . 4
Tfin Ncfin 1c ![_V](rmcv.gif) |
41 | | opklefing 4448 |
. . . 4
![(](lp.gif) ![(](lp.gif) Tfin Ncfin 1c ![_V](rmcv.gif)
![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) Tfin Ncfin 1c fin ![E.](exists.gif) Nn Tfin Ncfin 1c ![(](lp.gif)
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
42 | 39, 40, 41 | mp2an 653 |
. . 3
![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) Tfin Ncfin 1c fin ![E.](exists.gif) Nn Tfin Ncfin 1c ![(](lp.gif)
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
43 | 38, 42 | sylib 188 |
. 2
![(](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)
Nn Tfin
Ncfin 1c ![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
44 | | df1c2 4168 |
. . . . . . 7
1c
1 ![_V](rmcv.gif) |
45 | | pw1eq 4143 |
. . . . . . 7
1c 1 1 1c 1 1 ![_V](rmcv.gif) ![)](rp.gif) |
46 | 44, 45 | ax-mp 5 |
. . . . . 6
1
1c
1 1 ![_V](rmcv.gif) |
47 | | tfinpw1 4494 |
. . . . . . 7
![(](lp.gif) Ncfin
1c
Nn 1c Ncfin
1c
1
1c
Tfin Ncfin 1c![)](rp.gif) |
48 | 26, 47 | syl 15 |
. . . . . 6
![(](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) 1 1c Tfin Ncfin 1c![)](rp.gif) |
49 | 46, 48 | syl5eqelr 2438 |
. . . . 5
![(](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) 1 1 Tfin Ncfin 1c![)](rp.gif) |
50 | | eleq2 2414 |
. . . . 5
Tfin Ncfin 1c ![(](lp.gif)
![p](_p.gif) ![(](lp.gif) 1 1 Tfin Ncfin 1c 1 1 ![(](lp.gif)
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
51 | 49, 50 | syl5ibcom 211 |
. . . 4
![(](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) Tfin Ncfin 1c ![(](lp.gif)
![p](_p.gif) 1 1 ![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
52 | | eladdc 4398 |
. . . . 5
![(](lp.gif) 1 1 ![(](lp.gif) ![p](_p.gif)
![E.](exists.gif)
![E.](exists.gif)
![(](lp.gif) ![(](lp.gif) ![b](_b.gif) 1 1 ![(](lp.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
53 | | ssun1 3426 |
. . . . . . . . . . 11
![(](lp.gif)
![b](_b.gif) ![)](rp.gif) |
54 | | sseq2 3293 |
. . . . . . . . . . 11
![(](lp.gif) 1 1 ![(](lp.gif) ![b](_b.gif) ![(](lp.gif) 1 1 ![(](lp.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
55 | 53, 54 | mpbiri 224 |
. . . . . . . . . 10
![(](lp.gif) 1 1 ![(](lp.gif) ![b](_b.gif) 1 1 ![_V](rmcv.gif) ![)](rp.gif) |
56 | | vex 2862 |
. . . . . . . . . . . 12
![_V](rmcv.gif) |
57 | 56 | sspw1 4335 |
. . . . . . . . . . 11
![(](lp.gif) 1 1 ![E.](exists.gif) ![g](_g.gif) ![(](lp.gif)
1
1 ![g](_g.gif) ![)](rp.gif) ![)](rp.gif) |
58 | | vex 2862 |
. . . . . . . . . . . . . . . 16
![_V](rmcv.gif) |
59 | 58 | sspw1 4335 |
. . . . . . . . . . . . . . 15
![(](lp.gif) 1 ![E.](exists.gif) ![d](_d.gif) ![(](lp.gif)
1 ![d](_d.gif) ![)](rp.gif) ![)](rp.gif) |
60 | | ssv 3291 |
. . . . . . . . . . . . . . . . 17
![_V](rmcv.gif) |
61 | 60 | biantrur 492 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) 1
![(](lp.gif) 1 ![d](_d.gif) ![)](rp.gif) ![)](rp.gif) |
62 | 61 | exbii 1582 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![E.](exists.gif)
1 ![E.](exists.gif) ![d](_d.gif) ![(](lp.gif) 1 ![d](_d.gif) ![)](rp.gif) ![)](rp.gif) |
63 | 59, 62 | bitr4i 243 |
. . . . . . . . . . . . . 14
![(](lp.gif) 1 ![E.](exists.gif) 1 ![d](_d.gif) ![)](rp.gif) |
64 | 63 | anbi1i 676 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif)
1
1 ![g](_g.gif) ![(](lp.gif) ![E.](exists.gif) 1
1 ![g](_g.gif) ![)](rp.gif) ![)](rp.gif) |
65 | | 19.41v 1901 |
. . . . . . . . . . . . 13
![(](lp.gif) ![E.](exists.gif) ![d](_d.gif) ![(](lp.gif) 1
1 ![g](_g.gif) ![(](lp.gif) ![E.](exists.gif)
1
1 ![g](_g.gif) ![)](rp.gif) ![)](rp.gif) |
66 | 64, 65 | bitr4i 243 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif)
1
1 ![g](_g.gif) ![E.](exists.gif) ![d](_d.gif) ![(](lp.gif) 1
1 ![g](_g.gif) ![)](rp.gif) ![)](rp.gif) |
67 | 66 | exbii 1582 |
. . . . . . . . . . 11
![(](lp.gif) ![E.](exists.gif) ![g](_g.gif) ![(](lp.gif) 1 1 ![g](_g.gif) ![E.](exists.gif) ![g](_g.gif) ![E.](exists.gif) ![d](_d.gif) ![(](lp.gif)
1
1 ![g](_g.gif) ![)](rp.gif) ![)](rp.gif) |
68 | | excom 1741 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif) ![g](_g.gif) ![E.](exists.gif) ![d](_d.gif) ![(](lp.gif) 1
1 ![g](_g.gif) ![E.](exists.gif) ![d](_d.gif) ![E.](exists.gif) ![g](_g.gif) ![(](lp.gif) 1 1 ![g](_g.gif) ![)](rp.gif) ![)](rp.gif) |
69 | | vex 2862 |
. . . . . . . . . . . . . . 15
![_V](rmcv.gif) |
70 | 69 | pw1ex 4303 |
. . . . . . . . . . . . . 14
1 ![_V](rmcv.gif) |
71 | | pw1eq 4143 |
. . . . . . . . . . . . . . 15
![(](lp.gif) 1
1 1 1 ![d](_d.gif) ![)](rp.gif) |
72 | 71 | eqeq2d 2364 |
. . . . . . . . . . . . . 14
![(](lp.gif) 1
![(](lp.gif)
1 1 1 ![d](_d.gif) ![)](rp.gif) ![)](rp.gif) |
73 | 70, 72 | ceqsexv 2894 |
. . . . . . . . . . . . 13
![(](lp.gif) ![E.](exists.gif) ![g](_g.gif) ![(](lp.gif) 1
1 ![g](_g.gif) 1 1 ![d](_d.gif) ![)](rp.gif) |
74 | 73 | exbii 1582 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif) ![d](_d.gif) ![E.](exists.gif) ![g](_g.gif) ![(](lp.gif) 1
1 ![g](_g.gif) ![E.](exists.gif)
1 1 ![d](_d.gif) ![)](rp.gif) |
75 | 68, 74 | bitri 240 |
. . . . . . . . . . 11
![(](lp.gif) ![E.](exists.gif) ![g](_g.gif) ![E.](exists.gif) ![d](_d.gif) ![(](lp.gif) 1
1 ![g](_g.gif) ![E.](exists.gif)
1 1 ![d](_d.gif) ![)](rp.gif) |
76 | 57, 67, 75 | 3bitri 262 |
. . . . . . . . . 10
![(](lp.gif) 1 1 ![E.](exists.gif) 1 1 ![d](_d.gif) ![)](rp.gif) |
77 | 55, 76 | sylib 188 |
. . . . . . . . 9
![(](lp.gif) 1 1 ![(](lp.gif) ![b](_b.gif) ![E.](exists.gif)
1 1 ![d](_d.gif) ![)](rp.gif) |
78 | | eleq1 2413 |
. . . . . . . . . . . . 13
![(](lp.gif) 1 1
![(](lp.gif)
1 1 ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
79 | 78 | biimpac 472 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif)
1 1 ![d](_d.gif) 1 1
![z](_z.gif) ![)](rp.gif) |
80 | 32 | adantr 451 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](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) 1 1 ![z](_z.gif)
Nn ![)](rp.gif) |
81 | | ncfinprop 4474 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) Fin 1
![_V](rmcv.gif) Ncfin 1 Nn 1
Ncfin 1 ![d](_d.gif) ![)](rp.gif) ![)](rp.gif) |
82 | 70, 81 | mpan2 652 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) Fin Ncfin 1 Nn 1 Ncfin 1 ![d](_d.gif) ![)](rp.gif) ![)](rp.gif) |
83 | 82 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . 18
![(](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) Ncfin 1 Nn 1
Ncfin 1 ![d](_d.gif) ![)](rp.gif) ![)](rp.gif) |
84 | 83 | simpld 445 |
. . . . . . . . . . . . . . . . 17
![(](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) Ncfin 1 Nn ![)](rp.gif) |
85 | | tfincl 4492 |
. . . . . . . . . . . . . . . . 17
Ncfin 1 Nn Tfin Ncfin 1 Nn ![)](rp.gif) |
86 | 84, 85 | syl 15 |
. . . . . . . . . . . . . . . 16
![(](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) Tfin Ncfin 1 Nn ![)](rp.gif) |
87 | 86 | adantr 451 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](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) 1 1 ![z](_z.gif) Tfin
Ncfin 1
Nn ![)](rp.gif) |
88 | | simpr 447 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](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) 1 1 ![z](_z.gif) 1 1 ![z](_z.gif) ![)](rp.gif) |
89 | | tfinpw1 4494 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) Ncfin
1 Nn 1 Ncfin 1 ![d](_d.gif) 1 1 Tfin
Ncfin 1 ![d](_d.gif) ![)](rp.gif) |
90 | 83, 89 | syl 15 |
. . . . . . . . . . . . . . . 16
![(](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) 1 1 Tfin Ncfin 1 ![d](_d.gif) ![)](rp.gif) |
91 | 90 | adantr 451 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](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) 1 1 ![z](_z.gif) 1 1 Tfin Ncfin 1 ![d](_d.gif) ![)](rp.gif) |
92 | | nnceleq 4430 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Tfin Ncfin 1 Nn ![(](lp.gif) 1 1
1 1 Tfin Ncfin 1 ![d](_d.gif) ![)](rp.gif)
Tfin Ncfin 1 ![d](_d.gif) ![)](rp.gif) |
93 | 80, 87, 88, 91, 92 | syl22anc 1183 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](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) 1 1 ![z](_z.gif)
Tfin Ncfin 1 ![d](_d.gif) ![)](rp.gif) |
94 | 93 | ex 423 |
. . . . . . . . . . . . 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) ![(](lp.gif) 1 1
Tfin Ncfin 1 ![d](_d.gif) ![)](rp.gif) ![)](rp.gif) |
95 | 5 | ad2ant2r 727 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Tfin Spfin ![(](lp.gif)
Spfin Sfin Tfin Ncfin 1 ![d](_d.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif)
Nn ![)](rp.gif) |
96 | 69 | pwex 4329 |
. . . . . . . . . . . . . . . . . . . . . 22
![~P](scrp.gif) ![_V](rmcv.gif) |
97 | | ncfinprop 4474 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![(](lp.gif) Fin ![~P](scrp.gif) ![_V](rmcv.gif)
Ncfin ![~P](scrp.gif)
Nn ![~P](scrp.gif) Ncfin
![~P](scrp.gif) ![d](_d.gif) ![)](rp.gif) ![)](rp.gif) |
98 | 96, 97 | mpan2 652 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) Fin Ncfin ![~P](scrp.gif) Nn ![~P](scrp.gif)
Ncfin ![~P](scrp.gif) ![d](_d.gif) ![)](rp.gif) ![)](rp.gif) |
99 | 98 | simpld 445 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) Fin Ncfin ![~P](scrp.gif)
Nn ![)](rp.gif) |
100 | 99 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Tfin Spfin ![(](lp.gif)
Spfin Sfin Tfin Ncfin 1 ![d](_d.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) Ncfin ![~P](scrp.gif)
Nn ![)](rp.gif) |
101 | | simprr 733 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Tfin Spfin ![(](lp.gif)
Spfin Sfin Tfin Ncfin 1 ![d](_d.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) Sfin
Tfin Ncfin 1 ![d](_d.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
102 | 82 | simpld 445 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) Fin Ncfin 1 Nn ![)](rp.gif) |
103 | 82 | simprd 449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) Fin 1 Ncfin 1 ![d](_d.gif) ![)](rp.gif) |
104 | 98 | simprd 449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) Fin ![~P](scrp.gif)
Ncfin ![~P](scrp.gif) ![d](_d.gif) ![)](rp.gif) |
105 | | pw1eq 4143 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) 1 1 ![d](_d.gif) ![)](rp.gif) |
106 | 105 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![(](lp.gif) 1 Ncfin 1 1
Ncfin 1 ![d](_d.gif) ![)](rp.gif) ![)](rp.gif) |
107 | | pweq 3725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![~P](scrp.gif)
![~P](scrp.gif) ![d](_d.gif) ![)](rp.gif) |
108 | 107 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![(](lp.gif) ![~P](scrp.gif)
Ncfin ![~P](scrp.gif)
![~P](scrp.gif) Ncfin ![~P](scrp.gif) ![d](_d.gif) ![)](rp.gif) ![)](rp.gif) |
109 | 106, 108 | anbi12d 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1
Ncfin 1 ![~P](scrp.gif) Ncfin ![~P](scrp.gif) ![d](_d.gif) ![(](lp.gif) 1
Ncfin 1 ![~P](scrp.gif) Ncfin ![~P](scrp.gif) ![d](_d.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
110 | 69, 109 | spcev 2946 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif) 1
Ncfin 1 ![~P](scrp.gif) Ncfin ![~P](scrp.gif) ![d](_d.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) 1
Ncfin 1 ![~P](scrp.gif) Ncfin ![~P](scrp.gif) ![d](_d.gif) ![)](rp.gif) ![)](rp.gif) |
111 | 103, 104,
110 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) Fin ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) 1 Ncfin
1 ![~P](scrp.gif)
Ncfin ![~P](scrp.gif) ![d](_d.gif) ![)](rp.gif) ![)](rp.gif) |
112 | | df-sfin 4446 |
. . . . . . . . . . . . . . . . . . . . . . 23
Sfin Ncfin 1 ![d](_d.gif) Ncfin
![~P](scrp.gif) ![d](_d.gif) Ncfin 1 Nn Ncfin
![~P](scrp.gif) Nn ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) 1 Ncfin
1 ![~P](scrp.gif)
Ncfin ![~P](scrp.gif) ![d](_d.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
113 | 102, 99, 111, 112 | syl3anbrc 1136 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) Fin Sfin
Ncfin 1 ![d](_d.gif) Ncfin ![~P](scrp.gif) ![d](_d.gif) ![)](rp.gif) ![)](rp.gif) |
114 | 113 | ad2antrr 706 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Tfin Spfin ![(](lp.gif)
Spfin Sfin Tfin Ncfin 1 ![d](_d.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) Sfin
Ncfin 1 ![d](_d.gif) Ncfin ![~P](scrp.gif) ![d](_d.gif) ![)](rp.gif) ![)](rp.gif) |
115 | | sfintfin 4532 |
. . . . . . . . . . . . . . . . . . . . 21
Sfin Ncfin 1 ![d](_d.gif) Ncfin
![~P](scrp.gif) ![d](_d.gif) Sfin Tfin Ncfin 1 ![d](_d.gif) Tfin Ncfin ![~P](scrp.gif) ![d](_d.gif) ![)](rp.gif) ![)](rp.gif) |
116 | 114, 115 | syl 15 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Tfin Spfin ![(](lp.gif)
Spfin Sfin Tfin Ncfin 1 ![d](_d.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) Sfin
Tfin Ncfin 1 ![d](_d.gif) Tfin Ncfin ![~P](scrp.gif) ![d](_d.gif) ![)](rp.gif) ![)](rp.gif) |
117 | | sfin112 4529 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) Sfin
Tfin Ncfin 1 ![d](_d.gif) Tfin ![n](_n.gif)
Sfin Tfin Ncfin 1 ![d](_d.gif) Tfin Ncfin ![~P](scrp.gif) ![d](_d.gif) ![)](rp.gif) Tfin
Tfin Ncfin ![~P](scrp.gif) ![d](_d.gif) ![)](rp.gif) |
118 | 101, 116,
117 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Tfin Spfin ![(](lp.gif)
Spfin Sfin Tfin Ncfin 1 ![d](_d.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) Tfin
Tfin Ncfin ![~P](scrp.gif) ![d](_d.gif) ![)](rp.gif) |
119 | | tfin11 4493 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) Nn Ncfin ![~P](scrp.gif)
Nn Tfin Tfin
Ncfin ![~P](scrp.gif) ![d](_d.gif) Ncfin ![~P](scrp.gif) ![d](_d.gif) ![)](rp.gif) |
120 | 95, 100, 118, 119 | syl3anc 1182 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Tfin Spfin ![(](lp.gif)
Spfin Sfin Tfin Ncfin 1 ![d](_d.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif)
Ncfin ![~P](scrp.gif) ![d](_d.gif) ![)](rp.gif) |
121 | | simprl 732 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Tfin Spfin ![(](lp.gif)
Spfin Sfin Tfin Ncfin 1 ![d](_d.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif)
Spfin ![)](rp.gif) |
122 | 120, 121 | eqeltrrd 2428 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Tfin Spfin ![(](lp.gif)
Spfin Sfin Tfin Ncfin 1 ![d](_d.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) Ncfin ![~P](scrp.gif)
Spfin ![)](rp.gif) |
123 | | spfinsfincl 4539 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) Ncfin
![~P](scrp.gif) Spfin Sfin Ncfin 1 ![d](_d.gif) Ncfin
![~P](scrp.gif) ![d](_d.gif) ![)](rp.gif)
Ncfin 1 Spfin ![)](rp.gif) |
124 | 122, 114,
123 | syl2anc 642 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Tfin Spfin ![(](lp.gif)
Spfin Sfin Tfin Ncfin 1 ![d](_d.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) Ncfin 1 Spfin ![)](rp.gif) |
125 | | risset 2661 |
. . . . . . . . . . . . . . . . 17
Ncfin 1 Spfin ![E.](exists.gif)
Spfin
Ncfin 1 ![d](_d.gif) ![)](rp.gif) |
126 | | tfineq 4488 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) Ncfin 1 Tfin Tfin
Ncfin 1 ![d](_d.gif) ![)](rp.gif) |
127 | 126 | eqcomd 2358 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) Ncfin 1 Tfin Ncfin 1 Tfin ![x](_x.gif) ![)](rp.gif) |
128 | 127 | reximi 2721 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![E.](exists.gif)
Spfin Ncfin 1 ![E.](exists.gif) Spfin Tfin Ncfin 1 Tfin ![x](_x.gif) ![)](rp.gif) |
129 | 125, 128 | sylbi 187 |
. . . . . . . . . . . . . . . 16
Ncfin 1 Spfin ![E.](exists.gif) Spfin Tfin Ncfin 1 Tfin ![x](_x.gif) ![)](rp.gif) |
130 | 124, 129 | syl 15 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Tfin Spfin ![(](lp.gif)
Spfin Sfin Tfin Ncfin 1 ![d](_d.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif)
Spfin Tfin Ncfin 1 Tfin ![x](_x.gif) ![)](rp.gif) |
131 | | sfineq1 4526 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) Tfin Ncfin 1 Sfin ![(](lp.gif) ![z](_z.gif) Tfin ![n](_n.gif)
Sfin Tfin
Ncfin 1 ![d](_d.gif)
Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
132 | 131 | anbi2d 684 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) Tfin Ncfin 1 ![(](lp.gif) ![(](lp.gif) Spfin Sfin ![(](lp.gif) ![z](_z.gif) Tfin ![n](_n.gif) ![)](rp.gif)
![(](lp.gif) Spfin Sfin Tfin Ncfin 1 ![d](_d.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
133 | 132 | anbi2d 684 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) Tfin Ncfin 1 ![(](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) ![(](lp.gif) ![(](lp.gif) Fin Tfin Spfin ![(](lp.gif)
Spfin Sfin Tfin Ncfin 1 ![d](_d.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
134 | | eqeq1 2359 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) Tfin Ncfin 1 ![(](lp.gif) Tfin Tfin Ncfin 1 Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
135 | 134 | rexbidv 2635 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) Tfin Ncfin 1 ![(](lp.gif) ![E.](exists.gif)
Spfin Tfin ![E.](exists.gif)
Spfin Tfin Ncfin 1 Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
136 | 133, 135 | imbi12d 311 |
. . . . . . . . . . . . . . 15
![(](lp.gif) Tfin Ncfin 1 ![(](lp.gif) ![(](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) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin Tfin
Spfin ![(](lp.gif) Spfin
Sfin Tfin Ncfin 1 ![d](_d.gif) Tfin ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif)
Spfin Tfin Ncfin 1 Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
137 | 130, 136 | mpbiri 224 |
. . . . . . . . . . . . . 14
![(](lp.gif) Tfin Ncfin 1 ![(](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) ![)](rp.gif) |
138 | 137 | com12 27 |
. . . . . . . . . . . . 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) ![(](lp.gif)
Tfin Ncfin 1 ![E.](exists.gif) Spfin Tfin
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
139 | 94, 138 | syld 40 |
. . . . . . . . . . . 12
![(](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) ![(](lp.gif) 1 1 ![E.](exists.gif)
Spfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
140 | 79, 139 | syl5 28 |
. . . . . . . . . . 11
![(](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) ![(](lp.gif) ![(](lp.gif)
1 1 ![d](_d.gif) ![E.](exists.gif) Spfin Tfin
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
141 | 140 | expdimp 426 |
. . . . . . . . . 10
![(](lp.gif) ![(](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) ![z](_z.gif) ![(](lp.gif)
1 1 ![E.](exists.gif)
Spfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
142 | 141 | exlimdv 1636 |
. . . . . . . . 9
![(](lp.gif) ![(](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) ![z](_z.gif) ![(](lp.gif) ![E.](exists.gif)
1 1 ![E.](exists.gif) Spfin Tfin
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
143 | 77, 142 | syl5 28 |
. . . . . . . 8
![(](lp.gif) ![(](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) ![z](_z.gif) ![(](lp.gif) 1 1
![(](lp.gif) ![b](_b.gif) ![E.](exists.gif)
Spfin Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
144 | 143 | adantld 453 |
. . . . . . 7
![(](lp.gif) ![(](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) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![b](_b.gif)
1 1 ![(](lp.gif) ![b](_b.gif) ![)](rp.gif)
![E.](exists.gif) Spfin Tfin
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
145 | 144 | adantrr 697 |
. . . . . 6
![(](lp.gif) ![(](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) ![(](lp.gif)
![p](_p.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![b](_b.gif)
1 1 ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
![E.](exists.gif) Spfin Tfin
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
146 | 145 | rexlimdvva 2745 |
. . . . 5
![(](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) ![(](lp.gif) ![E.](exists.gif)
![E.](exists.gif)
![(](lp.gif) ![(](lp.gif) ![b](_b.gif)
1 1 ![(](lp.gif) ![b](_b.gif) ![)](rp.gif)
![E.](exists.gif) Spfin Tfin
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
147 | 52, 146 | syl5bi 208 |
. . . 4
![(](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) ![(](lp.gif) 1 1 ![(](lp.gif) ![p](_p.gif)
![E.](exists.gif) Spfin Tfin
![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
148 | 51, 147 | syld 40 |
. . 3
![(](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) Tfin Ncfin 1c ![(](lp.gif)
![p](_p.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
149 | 148 | rexlimdvw 2741 |
. 2
![(](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) ![(](lp.gif) ![E.](exists.gif)
Nn Tfin Ncfin 1c ![(](lp.gif)
![p](_p.gif) ![E.](exists.gif) Spfin
Tfin ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
150 | 43, 149 | mpd 14 |
1
![(](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) |