Step | Hyp | Ref
| Expression |
1 | | tfinltfinlem1 4500 |
. 2
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) fin Tfin ![M](_cm.gif)
Tfin ![N](_cn.gif) fin ![)](rp.gif) ![)](rp.gif) |
2 | | tfineq 4488 |
. . . . . . . . 9
![(](lp.gif)
Tfin
Tfin ![(/)](varnothing.gif) ![)](rp.gif) |
3 | | tfinnul 4491 |
. . . . . . . . 9
Tfin ![(/)](varnothing.gif) |
4 | 2, 3 | syl6eq 2401 |
. . . . . . . 8
![(](lp.gif)
Tfin
![(/)](varnothing.gif) ![)](rp.gif) |
5 | | df-ne 2518 |
. . . . . . . . 9
Tfin
Tfin
![(/)](varnothing.gif) ![)](rp.gif) |
6 | 5 | con2bii 322 |
. . . . . . . 8
Tfin
Tfin ![(/)](varnothing.gif) ![)](rp.gif) |
7 | 4, 6 | sylib 188 |
. . . . . . 7
![(](lp.gif)
Tfin ![(/)](varnothing.gif) ![)](rp.gif) |
8 | 7 | intnanrd 883 |
. . . . . 6
![(](lp.gif)
Tfin
![E.](exists.gif) Nn Tfin
![(](lp.gif) Tfin ![x](_x.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
9 | | tfinex 4485 |
. . . . . . 7
Tfin
![_V](rmcv.gif) |
10 | | tfinex 4485 |
. . . . . . 7
Tfin
![_V](rmcv.gif) |
11 | | opkltfing 4449 |
. . . . . . 7
![(](lp.gif) Tfin
Tfin ![_V](rmcv.gif) ![(](lp.gif) Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin Tfin
![E.](exists.gif) Nn Tfin
![(](lp.gif) Tfin ![x](_x.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
12 | 9, 10, 11 | mp2an 653 |
. . . . . 6
![(](lp.gif) Tfin ![M](_cm.gif)
Tfin ![N](_cn.gif) fin Tfin ![E.](exists.gif) Nn Tfin
![(](lp.gif) Tfin ![x](_x.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | 8, 12 | sylnibr 296 |
. . . . 5
![(](lp.gif)
Tfin ![M](_cm.gif)
Tfin ![N](_cn.gif) fin ![)](rp.gif) |
14 | 13 | pm2.21d 98 |
. . . 4
![(](lp.gif)
![(](lp.gif) Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) fin ![)](rp.gif) ![)](rp.gif) |
15 | 14 | a1d 22 |
. . 3
![(](lp.gif)
![(](lp.gif) ![(](lp.gif)
Nn Nn ![(](lp.gif) Tfin ![M](_cm.gif)
Tfin ![N](_cn.gif) fin ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
16 | | tfinprop 4489 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) Tfin Nn ![E.](exists.gif) 1 Tfin ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 16 | simpld 445 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) Tfin Nn ![)](rp.gif) |
18 | | ltfinirr 4457 |
. . . . . . . . . . . . 13
Tfin
Nn
Tfin ![M](_cm.gif) Tfin ![M](_cm.gif) fin ![)](rp.gif) |
19 | 17, 18 | syl 15 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif)
Tfin ![M](_cm.gif) Tfin ![M](_cm.gif) fin ![)](rp.gif) |
20 | 19 | 3adant2 974 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif)
Tfin ![M](_cm.gif) Tfin ![M](_cm.gif) fin ![)](rp.gif) |
21 | | opkeq2 4060 |
. . . . . . . . . . . . 13
Tfin
Tfin Tfin ![M](_cm.gif) Tfin ![M](_cm.gif) Tfin ![M](_cm.gif)
Tfin ![N](_cn.gif) ![>>](rrangle.gif) ![)](rp.gif) |
22 | 21 | eleq1d 2419 |
. . . . . . . . . . . 12
Tfin
Tfin ![(](lp.gif)
Tfin ![M](_cm.gif) Tfin ![M](_cm.gif) fin Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![)](rp.gif) ![)](rp.gif) |
23 | 22 | notbid 285 |
. . . . . . . . . . 11
Tfin
Tfin ![(](lp.gif) Tfin ![M](_cm.gif)
Tfin ![M](_cm.gif) fin
Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![)](rp.gif) ![)](rp.gif) |
24 | 20, 23 | syl5ibcom 211 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) Tfin Tfin Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![)](rp.gif) ![)](rp.gif) |
25 | 24 | con2d 107 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif)
Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin Tfin
Tfin ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 25 | imp 418 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin Tfin
Tfin ![N](_cn.gif) ![)](rp.gif) |
27 | | tfineq 4488 |
. . . . . . . 8
![(](lp.gif) Tfin
Tfin ![N](_cn.gif) ![)](rp.gif) |
28 | 26, 27 | nsyl 113 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![N](_cn.gif) ![)](rp.gif) |
29 | | simpl1 958 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif)
Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![(/)](varnothing.gif) ![)](rp.gif) Nn ![)](rp.gif) |
30 | | simpl3 960 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif)
Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![(/)](varnothing.gif) ![)](rp.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
31 | 29, 30, 17 | syl2anc 642 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif)
Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![(/)](varnothing.gif) ![)](rp.gif) Tfin Nn ![)](rp.gif) |
32 | | simpl2 959 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif)
Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![(/)](varnothing.gif) ![)](rp.gif) Nn ![)](rp.gif) |
33 | | simprr 733 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif)
Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![(/)](varnothing.gif) ![)](rp.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
34 | | tfinprop 4489 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) Tfin Nn ![E.](exists.gif) 1 Tfin ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 34 | simpld 445 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) Tfin Nn ![)](rp.gif) |
36 | 32, 33, 35 | syl2anc 642 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif)
Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![(/)](varnothing.gif) ![)](rp.gif) Tfin Nn ![)](rp.gif) |
37 | 31, 36 | jca 518 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif)
Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![(/)](varnothing.gif) ![)](rp.gif) Tfin
Nn Tfin Nn ![)](rp.gif) ![)](rp.gif) |
38 | | simprl 732 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif)
Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![(/)](varnothing.gif) ![)](rp.gif)
Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![)](rp.gif) |
39 | | ltfinasym 4460 |
. . . . . . . . . . 11
![(](lp.gif) Tfin
Nn Tfin
Nn ![(](lp.gif) Tfin ![M](_cm.gif)
Tfin ![N](_cn.gif) fin Tfin ![N](_cn.gif)
Tfin ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) |
40 | 37, 38, 39 | sylc 56 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif)
Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![(/)](varnothing.gif) ![)](rp.gif) Tfin ![N](_cn.gif)
Tfin ![M](_cm.gif) fin ![)](rp.gif) |
41 | 40 | expr 598 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![(](lp.gif)
Tfin ![N](_cn.gif)
Tfin ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) |
42 | | imnan 411 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Tfin ![N](_cn.gif)
Tfin ![M](_cm.gif) fin ![(](lp.gif)
Tfin ![N](_cn.gif)
Tfin ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) |
43 | 41, 42 | sylib 188 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![(](lp.gif)
Tfin ![N](_cn.gif)
Tfin ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) |
44 | | opkltfing 4449 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![(](lp.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 44 | ancoms 439 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![(](lp.gif)
![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
46 | 45 | 3adant3 975 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
47 | 46 | simprbda 606 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![(/)](varnothing.gif) ![)](rp.gif) |
48 | 47 | adantrl 696 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif)
Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![)](rp.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
49 | | simpl2 959 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif)
Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![)](rp.gif) Nn ![)](rp.gif) |
50 | | simpl1 958 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif)
Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![)](rp.gif) Nn ![)](rp.gif) |
51 | 49, 50 | jca 518 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif)
Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![)](rp.gif) ![(](lp.gif)
Nn Nn ![)](rp.gif) ![)](rp.gif) |
52 | | simprr 733 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif)
Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![)](rp.gif) ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![)](rp.gif) |
53 | | tfinltfinlem1 4500 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin Tfin ![N](_cn.gif)
Tfin ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) |
54 | 51, 52, 53 | sylc 56 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif)
Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![)](rp.gif) Tfin ![N](_cn.gif)
Tfin ![M](_cm.gif) fin ![)](rp.gif) |
55 | 48, 54 | jca 518 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif)
Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![)](rp.gif) ![(](lp.gif)
Tfin ![N](_cn.gif)
Tfin ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) |
56 | 55 | expr 598 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![(](lp.gif) ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![(](lp.gif)
Tfin ![N](_cn.gif)
Tfin ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
57 | 43, 56 | mtod 168 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![)](rp.gif) |
58 | | ltfintri 4466 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) fin ![<<](llangle.gif) ![N](_cn.gif) ![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) |
59 | 58 | adantr 451 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) fin
![<<](llangle.gif) ![N](_cn.gif)
![M](_cm.gif) fin ![)](rp.gif) ![)](rp.gif) |
60 | 28, 57, 59 | ecase23d 1285 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) fin ![)](rp.gif) |
61 | 60 | ex 423 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif)
Tfin ![M](_cm.gif) Tfin ![N](_cn.gif) fin ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) fin ![)](rp.gif) ![)](rp.gif) |
62 | 61 | 3expa 1151 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif) Tfin ![M](_cm.gif)
Tfin ![N](_cn.gif) fin ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) fin ![)](rp.gif) ![)](rp.gif) |
63 | 62 | expcom 424 |
. . 3
![(](lp.gif)
![(](lp.gif) ![(](lp.gif)
Nn Nn ![(](lp.gif) Tfin ![M](_cm.gif)
Tfin ![N](_cn.gif) fin ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
64 | 15, 63 | pm2.61ine 2592 |
. 2
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) Tfin ![M](_cm.gif)
Tfin ![N](_cn.gif) fin ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) fin ![)](rp.gif) ![)](rp.gif) |
65 | 1, 64 | impbid 183 |
1
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![M](_cm.gif) ![N](_cn.gif) fin Tfin ![M](_cm.gif)
Tfin ![N](_cn.gif) fin ![)](rp.gif) ![)](rp.gif) |