Step | Hyp | Ref
| Expression |
1 | | n0 3559 |
. . . 4
![(](lp.gif)
![E.](exists.gif)
![N](_cn.gif) ![)](rp.gif) |
2 | | simp2 956 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Fin Nn ![N](_cn.gif) Nn ![)](rp.gif) |
3 | | ncfinprop 4474 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Fin ![N](_cn.gif) Ncfin
Nn
Ncfin ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
4 | 3 | 3adant2 974 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Fin Nn ![N](_cn.gif) Ncfin
Nn
Ncfin ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
5 | 4 | simpld 445 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Fin Nn ![N](_cn.gif) Ncfin Nn ![)](rp.gif) |
6 | | simp3 957 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Fin Nn ![N](_cn.gif) ![N](_cn.gif) ![)](rp.gif) |
7 | 4 | simprd 449 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Fin Nn ![N](_cn.gif) Ncfin ![a](_a.gif) ![)](rp.gif) |
8 | | nnceleq 4430 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Ncfin Nn ![(](lp.gif)
Ncfin ![a](_a.gif) ![)](rp.gif) Ncfin ![a](_a.gif) ![)](rp.gif) |
9 | 2, 5, 6, 7, 8 | syl22anc 1183 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Fin Nn ![N](_cn.gif) Ncfin ![a](_a.gif) ![)](rp.gif) |
10 | 9 | 3expia 1153 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Fin Nn ![(](lp.gif) Ncfin ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
11 | | simpr 447 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Fin Ncfin ![a](_a.gif)
Ncfin ![a](_a.gif) ![)](rp.gif) |
12 | | uncompl 4074 |
. . . . . . . . . . . . 13
![(](lp.gif) ∼ ![a](_a.gif) ![_V](rmcv.gif) |
13 | | ncfineq 4473 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ∼
![a](_a.gif) Ncfin ![(](lp.gif)
∼ ![a](_a.gif) Ncfin ![_V](rmcv.gif) ![)](rp.gif) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . . . 12
Ncfin ![(](lp.gif)
∼ ![a](_a.gif) Ncfin ![_V](rmcv.gif) |
15 | | vex 2862 |
. . . . . . . . . . . . 13
![_V](rmcv.gif) |
16 | 15 | complex 4104 |
. . . . . . . . . . . . . 14
∼ ![_V](rmcv.gif) |
17 | | incompl 4073 |
. . . . . . . . . . . . . 14
![(](lp.gif) ∼ ![a](_a.gif) ![(/)](varnothing.gif) |
18 | | ncfindi 4475 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Fin ![_V](rmcv.gif) ∼ ![(](lp.gif) ∼ ![a](_a.gif)
![(/)](varnothing.gif) Ncfin ![(](lp.gif)
∼ ![a](_a.gif) Ncfin Ncfin ∼ ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
19 | 16, 17, 18 | mp3an23 1269 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Fin ![_V](rmcv.gif) Ncfin ![(](lp.gif) ∼ ![a](_a.gif) Ncfin Ncfin ∼ ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
20 | 15, 19 | mpan2 652 |
. . . . . . . . . . . 12
![(](lp.gif) Fin Ncfin ![(](lp.gif)
∼ ![a](_a.gif) Ncfin Ncfin ∼ ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 14, 20 | syl5eqr 2399 |
. . . . . . . . . . 11
![(](lp.gif) Fin Ncfin
Ncfin Ncfin ∼ ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 21 | adantr 451 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Fin Ncfin ![a](_a.gif)
Ncfin
Ncfin Ncfin ∼ ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 11, 22 | opkeq12d 4067 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Fin Ncfin ![a](_a.gif)
![<<](llangle.gif) ![N](_cn.gif) Ncfin ![_V](rmcv.gif) Ncfin ![a](_a.gif)
Ncfin Ncfin ∼ ![a](_a.gif) ![)](rp.gif) ![>>](rrangle.gif) ![)](rp.gif) |
24 | | ncfinex 4472 |
. . . . . . . . . . 11
Ncfin
![_V](rmcv.gif) |
25 | | ncfinprop 4474 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Fin ∼ ![_V](rmcv.gif) Ncfin ∼ Nn ∼
Ncfin ∼ ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 16, 25 | mpan2 652 |
. . . . . . . . . . . 12
![(](lp.gif) Fin Ncfin ∼ Nn ∼ Ncfin
∼ ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
27 | 26 | simpld 445 |
. . . . . . . . . . 11
![(](lp.gif) Fin Ncfin ∼ Nn ![)](rp.gif) |
28 | | lefinaddc 4450 |
. . . . . . . . . . 11
![(](lp.gif) Ncfin
Ncfin ∼ Nn Ncfin ![a](_a.gif) Ncfin Ncfin ∼ ![a](_a.gif) ![)](rp.gif) fin ![)](rp.gif) |
29 | 24, 27, 28 | sylancr 644 |
. . . . . . . . . 10
![(](lp.gif) Fin Ncfin ![a](_a.gif) Ncfin Ncfin ∼ ![a](_a.gif) ![)](rp.gif) fin ![)](rp.gif) |
30 | 29 | adantr 451 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Fin Ncfin ![a](_a.gif)
Ncfin ![a](_a.gif)
Ncfin Ncfin ∼ ![a](_a.gif) ![)](rp.gif) fin ![)](rp.gif) |
31 | 23, 30 | eqeltrd 2427 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Fin Ncfin ![a](_a.gif)
![<<](llangle.gif) ![N](_cn.gif) Ncfin ![_V](rmcv.gif) fin ![)](rp.gif) |
32 | 31 | ex 423 |
. . . . . . 7
![(](lp.gif) Fin ![(](lp.gif)
Ncfin ![<<](llangle.gif) ![N](_cn.gif) Ncfin ![_V](rmcv.gif) fin ![)](rp.gif) ![)](rp.gif) |
33 | 32 | adantr 451 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Fin Nn ![(](lp.gif) Ncfin ![<<](llangle.gif) ![N](_cn.gif) Ncfin ![_V](rmcv.gif) fin ![)](rp.gif) ![)](rp.gif) |
34 | 10, 33 | syld 40 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Fin Nn ![(](lp.gif) ![<<](llangle.gif) ![N](_cn.gif) Ncfin ![_V](rmcv.gif) fin ![)](rp.gif) ![)](rp.gif) |
35 | 34 | exlimdv 1636 |
. . . 4
![(](lp.gif) ![(](lp.gif) Fin Nn ![(](lp.gif) ![E.](exists.gif)
![<<](llangle.gif) ![N](_cn.gif) Ncfin ![_V](rmcv.gif) fin ![)](rp.gif) ![)](rp.gif) |
36 | 1, 35 | syl5bi 208 |
. . 3
![(](lp.gif) ![(](lp.gif) Fin Nn ![(](lp.gif)
![<<](llangle.gif) ![N](_cn.gif) Ncfin ![_V](rmcv.gif) fin ![)](rp.gif) ![)](rp.gif) |
37 | 36 | 3impia 1148 |
. 2
![(](lp.gif) ![(](lp.gif) Fin Nn ![(/)](varnothing.gif) ![<<](llangle.gif) ![N](_cn.gif) Ncfin ![_V](rmcv.gif) fin ![)](rp.gif) |
38 | | simp2 956 |
. . . 4
![(](lp.gif) ![(](lp.gif) Fin Nn ![(/)](varnothing.gif) Nn ![)](rp.gif) |
39 | | vvex 4109 |
. . . . . . 7
![_V](rmcv.gif) |
40 | | ncfinprop 4474 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Fin ![_V](rmcv.gif) Ncfin Nn Ncfin ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
41 | 39, 40 | mpan2 652 |
. . . . . 6
![(](lp.gif) Fin Ncfin Nn Ncfin ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
42 | 41 | 3ad2ant1 976 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Fin Nn ![(/)](varnothing.gif) Ncfin Nn Ncfin ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
43 | 42 | simpld 445 |
. . . 4
![(](lp.gif) ![(](lp.gif) Fin Nn ![(/)](varnothing.gif) Ncfin Nn ![)](rp.gif) |
44 | | tfinlefin 4502 |
. . . 4
![(](lp.gif) ![(](lp.gif) Nn Ncfin Nn ![(](lp.gif) ![<<](llangle.gif) ![N](_cn.gif) Ncfin ![_V](rmcv.gif) fin Tfin ![N](_cn.gif)
Tfin Ncfin ![_V](rmcv.gif) fin ![)](rp.gif) ![)](rp.gif) |
45 | 38, 43, 44 | syl2anc 642 |
. . 3
![(](lp.gif) ![(](lp.gif) Fin Nn ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![N](_cn.gif) Ncfin ![_V](rmcv.gif) fin Tfin ![N](_cn.gif)
Tfin Ncfin ![_V](rmcv.gif) fin ![)](rp.gif) ![)](rp.gif) |
46 | | tncveqnc1fin 4544 |
. . . . . 6
![(](lp.gif) Fin Tfin
Ncfin Ncfin
1c![)](rp.gif) |
47 | 46 | 3ad2ant1 976 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Fin Nn ![(/)](varnothing.gif) Tfin Ncfin
Ncfin 1c![)](rp.gif) |
48 | 47 | opkeq2d 4066 |
. . . 4
![(](lp.gif) ![(](lp.gif) Fin Nn ![(/)](varnothing.gif) Tfin ![N](_cn.gif) Tfin Ncfin ![_V](rmcv.gif) Tfin ![N](_cn.gif)
Ncfin 1c![>>](rrangle.gif) ![)](rp.gif) |
49 | 48 | eleq1d 2419 |
. . 3
![(](lp.gif) ![(](lp.gif) Fin Nn ![(/)](varnothing.gif) ![(](lp.gif)
Tfin ![N](_cn.gif) Tfin Ncfin ![_V](rmcv.gif) fin Tfin ![N](_cn.gif)
Ncfin 1c fin ![)](rp.gif) ![)](rp.gif) |
50 | 45, 49 | bitrd 244 |
. 2
![(](lp.gif) ![(](lp.gif) Fin Nn ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![N](_cn.gif) Ncfin ![_V](rmcv.gif) fin Tfin ![N](_cn.gif)
Ncfin 1c fin ![)](rp.gif) ![)](rp.gif) |
51 | 37, 50 | mpbid 201 |
1
![(](lp.gif) ![(](lp.gif) Fin Nn ![(/)](varnothing.gif) Tfin ![N](_cn.gif) Ncfin 1c fin ![)](rp.gif) |