Proof of Theorem lenltfin
Step | Hyp | Ref
| Expression |
1 | | ltfinirr 4457 |
. . . . . 6
![(](lp.gif) Nn ![<<](llangle.gif) ![A](_ca.gif) ![A](_ca.gif) fin ![)](rp.gif) |
2 | 1 | adantr 451 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nn Nn ![<<](llangle.gif) ![A](_ca.gif) ![A](_ca.gif) fin ![)](rp.gif) |
3 | 2 | adantr 451 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![A](_ca.gif) fin ![)](rp.gif) |
4 | | leltfintr 4458 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Nn Nn Nn ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![<<](llangle.gif) ![B](_cb.gif) ![A](_ca.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![A](_ca.gif) fin ![)](rp.gif) ![)](rp.gif) |
5 | 4 | 3anidm13 1240 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![<<](llangle.gif) ![B](_cb.gif) ![A](_ca.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![A](_ca.gif) fin ![)](rp.gif) ![)](rp.gif) |
6 | 5 | expdimp 426 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![(](lp.gif) ![<<](llangle.gif) ![B](_cb.gif) ![A](_ca.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![A](_ca.gif) fin ![)](rp.gif) ![)](rp.gif) |
7 | 3, 6 | mtod 168 |
. . 3
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![<<](llangle.gif) ![B](_cb.gif) ![A](_ca.gif) fin ![)](rp.gif) |
8 | 7 | ex 423 |
. 2
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![<<](llangle.gif) ![B](_cb.gif) ![A](_ca.gif) fin ![)](rp.gif) ![)](rp.gif) |
9 | | nulge 4456 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Nn Nn ![<<](llangle.gif) ![A](_ca.gif) ![(/)](varnothing.gif) fin ![)](rp.gif) |
10 | 9 | ancoms 439 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nn
Nn ![<<](llangle.gif) ![A](_ca.gif) ![(/)](varnothing.gif) fin ![)](rp.gif) |
11 | | eleq1 2413 |
. . . . . . 7
![(](lp.gif)
![(](lp.gif)
Nn Nn ![)](rp.gif) ![)](rp.gif) |
12 | 11 | anbi2d 684 |
. . . . . 6
![(](lp.gif)
![(](lp.gif) ![(](lp.gif)
Nn Nn ![(](lp.gif) Nn Nn ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | | opkeq2 4060 |
. . . . . . 7
![(](lp.gif)
![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![<<](llangle.gif) ![A](_ca.gif) ![(/)](varnothing.gif) ![>>](rrangle.gif) ![)](rp.gif) |
14 | 13 | eleq1d 2419 |
. . . . . 6
![(](lp.gif)
![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![(/)](varnothing.gif) fin ![)](rp.gif) ![)](rp.gif) |
15 | 12, 14 | imbi12d 311 |
. . . . 5
![(](lp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![(](lp.gif) ![(](lp.gif) Nn
Nn ![<<](llangle.gif) ![A](_ca.gif) ![(/)](varnothing.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
16 | 10, 15 | mpbiri 224 |
. . . 4
![(](lp.gif)
![(](lp.gif) ![(](lp.gif)
Nn Nn ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![)](rp.gif) ![)](rp.gif) |
17 | 16 | a1dd 42 |
. . 3
![(](lp.gif)
![(](lp.gif) ![(](lp.gif)
Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![B](_cb.gif) ![A](_ca.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
18 | | simplr 731 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) Nn ![)](rp.gif) |
19 | | simpll 730 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) Nn ![)](rp.gif) |
20 | | simpr 447 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
21 | | ltfintri 4466 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![B](_cb.gif) ![A](_ca.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![)](rp.gif) ![)](rp.gif) |
22 | 18, 19, 20, 21 | syl3anc 1182 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![B](_cb.gif) ![A](_ca.gif) fin
![<<](llangle.gif) ![A](_ca.gif)
![B](_cb.gif) fin ![)](rp.gif) ![)](rp.gif) |
23 | | 3orass 937 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![B](_cb.gif) ![A](_ca.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![(](lp.gif) ![<<](llangle.gif) ![B](_cb.gif) ![A](_ca.gif) fin ![(](lp.gif)
![<<](llangle.gif) ![A](_ca.gif)
![B](_cb.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 22, 23 | sylib 188 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![B](_cb.gif) ![A](_ca.gif) fin ![(](lp.gif)
![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 24 | ord 366 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![B](_cb.gif) ![A](_ca.gif) fin ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
26 | | lefinrflx 4467 |
. . . . . . . . 9
![(](lp.gif) Nn ![<<](llangle.gif) ![A](_ca.gif) ![A](_ca.gif) fin ![)](rp.gif) |
27 | 26 | adantr 451 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Nn Nn ![<<](llangle.gif) ![A](_ca.gif) ![A](_ca.gif) fin ![)](rp.gif) |
28 | | opkeq2 4060 |
. . . . . . . . 9
![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![<<](llangle.gif) ![A](_ca.gif) ![A](_ca.gif) ![>>](rrangle.gif) ![)](rp.gif) |
29 | 28 | eleq1d 2419 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![A](_ca.gif) fin ![)](rp.gif) ![)](rp.gif) |
30 | 27, 29 | syl5ibrcom 213 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![)](rp.gif) ![)](rp.gif) |
31 | 30 | adantr 451 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![)](rp.gif) ![)](rp.gif) |
32 | | ltlefin 4468 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![<<](llangle.gif) ![A](_ca.gif)
![B](_cb.gif) fin ![)](rp.gif) ![)](rp.gif) |
33 | 32 | adantr 451 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![<<](llangle.gif) ![A](_ca.gif)
![B](_cb.gif) fin ![)](rp.gif) ![)](rp.gif) |
34 | 31, 33 | jaod 369 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif)
![B](_cb.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![)](rp.gif) ![)](rp.gif) |
35 | 25, 34 | syld 40 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(/)](varnothing.gif) ![(](lp.gif) ![<<](llangle.gif) ![B](_cb.gif) ![A](_ca.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![)](rp.gif) ![)](rp.gif) |
36 | 35 | expcom 424 |
. . 3
![(](lp.gif)
![(](lp.gif) ![(](lp.gif)
Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![B](_cb.gif) ![A](_ca.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 17, 36 | pm2.61ine 2592 |
. 2
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![B](_cb.gif) ![A](_ca.gif) fin ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![)](rp.gif) ![)](rp.gif) |
38 | 8, 37 | impbid 183 |
1
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) fin ![<<](llangle.gif) ![B](_cb.gif) ![A](_ca.gif) fin ![)](rp.gif) ![)](rp.gif) |