Step | Hyp | Ref
| Expression |
1 | | lmxrge0.j |
. . . . . . 7
↾s |
2 | | eqid 2622 |
. . . . . . . 8
↾s
↾s |
3 | | xrstopn 21012 |
. . . . . . . 8
ordTop |
4 | 2, 3 | resstopn 20990 |
. . . . . . 7
ordTop
↾t ↾s
|
5 | 1, 4 | eqtr4i 2647 |
. . . . . 6
ordTop ↾t |
6 | | letopon 21009 |
. . . . . . 7
ordTop TopOn |
7 | | iccssxr 12256 |
. . . . . . 7
|
8 | | resttopon 20965 |
. . . . . . 7
ordTop
TopOn ordTop ↾t TopOn
|
9 | 6, 7, 8 | mp2an 708 |
. . . . . 6
ordTop
↾t TopOn |
10 | 5, 9 | eqeltri 2697 |
. . . . 5
TopOn |
11 | 10 | a1i 11 |
. . . 4
TopOn |
12 | | nnuz 11723 |
. . . 4
|
13 | | 1zzd 11408 |
. . . 4
|
14 | | lmxrge0.6 |
. . . 4
|
15 | | lmxrge0.7 |
. . . 4
|
16 | 11, 12, 13, 14, 15 | lmbrf 21064 |
. . 3
|
17 | | 0xr 10086 |
. . . . 5
|
18 | | pnfxr 10092 |
. . . . 5
|
19 | | 0lepnf 11966 |
. . . . 5
|
20 | | ubicc2 12289 |
. . . . 5
|
21 | 17, 18, 19, 20 | mp3an 1424 |
. . . 4
|
22 | 21 | biantrur 527 |
. . 3
|
23 | 16, 22 | syl6bbr 278 |
. 2
|
24 | | rexr 10085 |
. . . . . . . . . 10
|
25 | 18 | a1i 11 |
. . . . . . . . . 10
|
26 | | ltpnf 11954 |
. . . . . . . . . 10
|
27 | | ubioc1 12227 |
. . . . . . . . . 10
|
28 | 24, 25, 26, 27 | syl3anc 1326 |
. . . . . . . . 9
|
29 | | 0ltpnf 11956 |
. . . . . . . . . 10
|
30 | | ubioc1 12227 |
. . . . . . . . . 10
|
31 | 17, 18, 29, 30 | mp3an 1424 |
. . . . . . . . 9
|
32 | 28, 31 | jctir 561 |
. . . . . . . 8
|
33 | | elin 3796 |
. . . . . . . 8
|
34 | 32, 33 | sylibr 224 |
. . . . . . 7
|
35 | 34 | ad2antlr 763 |
. . . . . 6
|
36 | | letop 21010 |
. . . . . . . . . . 11
ordTop |
37 | | ovex 6678 |
. . . . . . . . . . 11
|
38 | | iocpnfordt 21019 |
. . . . . . . . . . . 12
ordTop
|
39 | | iocpnfordt 21019 |
. . . . . . . . . . . 12
ordTop
|
40 | | inopn 20704 |
. . . . . . . . . . . 12
ordTop
ordTop
ordTop
ordTop |
41 | 36, 38, 39, 40 | mp3an 1424 |
. . . . . . . . . . 11
ordTop |
42 | | elrestr 16089 |
. . . . . . . . . . 11
ordTop
ordTop
ordTop
↾t |
43 | 36, 37, 41, 42 | mp3an 1424 |
. . . . . . . . . 10
ordTop
↾t |
44 | | inss2 3834 |
. . . . . . . . . . . . 13
|
45 | | iocssicc 12261 |
. . . . . . . . . . . . 13
|
46 | 44, 45 | sstri 3612 |
. . . . . . . . . . . 12
|
47 | | sseqin2 3817 |
. . . . . . . . . . . 12
|
48 | 46, 47 | mpbi 220 |
. . . . . . . . . . 11
|
49 | | incom 3805 |
. . . . . . . . . . 11
|
50 | 48, 49 | eqtr3i 2646 |
. . . . . . . . . 10
|
51 | 43, 50, 5 | 3eltr4i 2714 |
. . . . . . . . 9
|
52 | 51 | a1i 11 |
. . . . . . . 8
|
53 | | eleq2 2690 |
. . . . . . . . . . 11
|
54 | 53 | adantl 482 |
. . . . . . . . . 10
|
55 | 54 | biimprd 238 |
. . . . . . . . 9
|
56 | | simp-5r 809 |
. . . . . . . . . . . . . . 15
|
57 | 56 | rexrd 10089 |
. . . . . . . . . . . . . 14
|
58 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
59 | | simp-4r 807 |
. . . . . . . . . . . . . . . 16
|
60 | 58, 59 | eleqtrd 2703 |
. . . . . . . . . . . . . . 15
|
61 | | elin 3796 |
. . . . . . . . . . . . . . . 16
|
62 | 61 | simplbi 476 |
. . . . . . . . . . . . . . 15
|
63 | 60, 62 | syl 17 |
. . . . . . . . . . . . . 14
|
64 | | elioc1 12217 |
. . . . . . . . . . . . . . . . 17
|
65 | 18, 64 | mpan2 707 |
. . . . . . . . . . . . . . . 16
|
66 | 65 | biimpa 501 |
. . . . . . . . . . . . . . 15
|
67 | 66 | simp2d 1074 |
. . . . . . . . . . . . . 14
|
68 | 57, 63, 67 | syl2anc 693 |
. . . . . . . . . . . . 13
|
69 | 68 | ex 450 |
. . . . . . . . . . . 12
|
70 | 69 | ralimdva 2962 |
. . . . . . . . . . 11
|
71 | 70 | reximdva 3017 |
. . . . . . . . . 10
|
72 | | fveq2 6191 |
. . . . . . . . . . . 12
|
73 | 72 | raleqdv 3144 |
. . . . . . . . . . 11
|
74 | 73 | cbvrexv 3172 |
. . . . . . . . . 10
|
75 | 71, 74 | syl6ibr 242 |
. . . . . . . . 9
|
76 | 55, 75 | imim12d 81 |
. . . . . . . 8
|
77 | 52, 76 | rspcimdv 3310 |
. . . . . . 7
|
78 | 77 | imp 445 |
. . . . . 6
|
79 | 35, 78 | mpd 15 |
. . . . 5
|
80 | 79 | ex 450 |
. . . 4
|
81 | 80 | ralrimdva 2969 |
. . 3
|
82 | | simplll 798 |
. . . . . 6
|
83 | | simpllr 799 |
. . . . . . 7
|
84 | | simpr 477 |
. . . . . . 7
|
85 | 1 | pnfneige0 29997 |
. . . . . . 7
|
86 | 83, 84, 85 | syl2anc 693 |
. . . . . 6
|
87 | | simplr 792 |
. . . . . 6
|
88 | | r19.29r 3073 |
. . . . . . . 8
|
89 | | simp-4l 806 |
. . . . . . . . . . . . . . 15
|
90 | | uznnssnn 11735 |
. . . . . . . . . . . . . . . . 17
|
91 | 90 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
|
92 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
93 | 91, 92 | sseldd 3604 |
. . . . . . . . . . . . . . 15
|
94 | 89, 93 | jca 554 |
. . . . . . . . . . . . . 14
|
95 | | simp-4r 807 |
. . . . . . . . . . . . . 14
|
96 | | simpllr 799 |
. . . . . . . . . . . . . 14
|
97 | | simplr 792 |
. . . . . . . . . . . . . . . 16
|
98 | | simplr 792 |
. . . . . . . . . . . . . . . . . . 19
|
99 | 98 | rexrd 10089 |
. . . . . . . . . . . . . . . . . 18
|
100 | 14 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . 21
|
101 | 15, 100 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . . 20
|
102 | 7, 101 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . 19
|
103 | 102 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
104 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
105 | | pnfge 11964 |
. . . . . . . . . . . . . . . . . . 19
|
106 | 103, 105 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
107 | 65 | biimpar 502 |
. . . . . . . . . . . . . . . . . 18
|
108 | 99, 103, 104, 106, 107 | syl13anc 1328 |
. . . . . . . . . . . . . . . . 17
|
109 | 108 | adantlr 751 |
. . . . . . . . . . . . . . . 16
|
110 | 97, 109 | sseldd 3604 |
. . . . . . . . . . . . . . 15
|
111 | 110 | ex 450 |
. . . . . . . . . . . . . 14
|
112 | 94, 95, 96, 111 | syl21anc 1325 |
. . . . . . . . . . . . 13
|
113 | 112 | ralimdva 2962 |
. . . . . . . . . . . 12
|
114 | 113 | reximdva 3017 |
. . . . . . . . . . 11
|
115 | 74, 114 | syl5bi 232 |
. . . . . . . . . 10
|
116 | 115 | expimpd 629 |
. . . . . . . . 9
|
117 | 116 | rexlimdva 3031 |
. . . . . . . 8
|
118 | 88, 117 | syl5 34 |
. . . . . . 7
|
119 | 118 | imp 445 |
. . . . . 6
|
120 | 82, 86, 87, 119 | syl12anc 1324 |
. . . . 5
|
121 | 120 | exp31 630 |
. . . 4
|
122 | 121 | ralrimdva 2969 |
. . 3
|
123 | 81, 122 | impbid 202 |
. 2
|
124 | 23, 123 | bitrd 268 |
1
|