Step | Hyp | Ref
| Expression |
1 | | islptre.1 |
. . . . . 6
|
2 | | retopon 22567 |
. . . . . 6
TopOn |
3 | 1, 2 | eqeltri 2697 |
. . . . 5
TopOn |
4 | 3 | topontopi 20720 |
. . . 4
|
5 | 4 | a1i 11 |
. . 3
|
6 | | islptre.2 |
. . 3
|
7 | | islptre.3 |
. . 3
|
8 | 3 | toponunii 20721 |
. . . 4
|
9 | 8 | islp2 20949 |
. . 3
|
10 | 5, 6, 7, 9 | syl3anc 1326 |
. 2
|
11 | | simp1r 1086 |
. . . . . 6
|
12 | | iooretop 22569 |
. . . . . . . . . . . 12
|
13 | 12, 1 | eleqtrri 2700 |
. . . . . . . . . . 11
|
14 | 13 | a1i 11 |
. . . . . . . . . 10
|
15 | | snssi 4339 |
. . . . . . . . . . 11
|
16 | 15 | adantl 482 |
. . . . . . . . . 10
|
17 | | ssid 3624 |
. . . . . . . . . . 11
|
18 | 17 | a1i 11 |
. . . . . . . . . 10
|
19 | | sseq2 3627 |
. . . . . . . . . . . 12
|
20 | | sseq1 3626 |
. . . . . . . . . . . 12
|
21 | 19, 20 | anbi12d 747 |
. . . . . . . . . . 11
|
22 | 21 | rspcev 3309 |
. . . . . . . . . 10
|
23 | 14, 16, 18, 22 | syl12anc 1324 |
. . . . . . . . 9
|
24 | | ioossre 12235 |
. . . . . . . . 9
|
25 | 23, 24 | jctil 560 |
. . . . . . . 8
|
26 | | elioore 12205 |
. . . . . . . . . . 11
|
27 | 26 | snssd 4340 |
. . . . . . . . . 10
|
28 | 27 | adantl 482 |
. . . . . . . . 9
|
29 | 8 | isnei 20907 |
. . . . . . . . 9
|
30 | 4, 28, 29 | sylancr 695 |
. . . . . . . 8
|
31 | 25, 30 | mpbird 247 |
. . . . . . 7
|
32 | 31 | 3adant1 1079 |
. . . . . 6
|
33 | | ineq1 3807 |
. . . . . . . 8
|
34 | 33 | neeq1d 2853 |
. . . . . . 7
|
35 | 34 | rspccva 3308 |
. . . . . 6
|
36 | 11, 32, 35 | syl2anc 693 |
. . . . 5
|
37 | 36 | 3exp 1264 |
. . . 4
|
38 | 37 | ralrimivv 2970 |
. . 3
|
39 | 7 | snssd 4340 |
. . . . . . . . 9
|
40 | 8 | isnei 20907 |
. . . . . . . . 9
|
41 | 4, 39, 40 | sylancr 695 |
. . . . . . . 8
|
42 | 41 | simplbda 654 |
. . . . . . 7
|
43 | 1 | eleq2i 2693 |
. . . . . . . . . . . . . . 15
|
44 | 43 | biimpi 206 |
. . . . . . . . . . . . . 14
|
45 | 44 | 3ad2ant2 1083 |
. . . . . . . . . . . . 13
|
46 | | simp1 1061 |
. . . . . . . . . . . . . 14
|
47 | | simp3l 1089 |
. . . . . . . . . . . . . 14
|
48 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
49 | 7 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
50 | | snssg 4327 |
. . . . . . . . . . . . . . . 16
|
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . 15
|
52 | 48, 51 | mpbird 247 |
. . . . . . . . . . . . . 14
|
53 | 46, 47, 52 | syl2anc 693 |
. . . . . . . . . . . . 13
|
54 | 45, 53 | jca 554 |
. . . . . . . . . . . 12
|
55 | | tg2 20769 |
. . . . . . . . . . . 12
|
56 | | ioof 12271 |
. . . . . . . . . . . . . . . . 17
|
57 | | ffn 6045 |
. . . . . . . . . . . . . . . . 17
|
58 | | ovelrn 6810 |
. . . . . . . . . . . . . . . . 17
|
59 | 56, 57, 58 | mp2b 10 |
. . . . . . . . . . . . . . . 16
|
60 | 59 | biimpi 206 |
. . . . . . . . . . . . . . 15
|
61 | 60 | adantr 481 |
. . . . . . . . . . . . . 14
|
62 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . 20
|
63 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
64 | 62, 63 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . 19
|
65 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . 20
|
66 | 63, 65 | eqsstr3d 3640 |
. . . . . . . . . . . . . . . . . . 19
|
67 | 64, 66 | jca 554 |
. . . . . . . . . . . . . . . . . 18
|
68 | 67 | ex 450 |
. . . . . . . . . . . . . . . . 17
|
69 | 68 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
70 | 69 | reximdv 3016 |
. . . . . . . . . . . . . . 15
|
71 | 70 | reximdv 3016 |
. . . . . . . . . . . . . 14
|
72 | 61, 71 | mpd 15 |
. . . . . . . . . . . . 13
|
73 | 72 | rexlimiva 3028 |
. . . . . . . . . . . 12
|
74 | 54, 55, 73 | 3syl 18 |
. . . . . . . . . . 11
|
75 | | simpl3r 1117 |
. . . . . . . . . . . . . . . 16
|
76 | 75 | adantr 481 |
. . . . . . . . . . . . . . 15
|
77 | | sstr 3611 |
. . . . . . . . . . . . . . . 16
|
78 | 77 | expcom 451 |
. . . . . . . . . . . . . . 15
|
79 | 76, 78 | syl 17 |
. . . . . . . . . . . . . 14
|
80 | 79 | anim2d 589 |
. . . . . . . . . . . . 13
|
81 | 80 | reximdva 3017 |
. . . . . . . . . . . 12
|
82 | 81 | reximdva 3017 |
. . . . . . . . . . 11
|
83 | 74, 82 | mpd 15 |
. . . . . . . . . 10
|
84 | 83 | 3exp 1264 |
. . . . . . . . 9
|
85 | 84 | rexlimdv 3030 |
. . . . . . . 8
|
86 | 85 | adantr 481 |
. . . . . . 7
|
87 | 42, 86 | mpd 15 |
. . . . . 6
|
88 | 87 | adantlr 751 |
. . . . 5
|
89 | | nfv 1843 |
. . . . . . . 8
|
90 | | nfra1 2941 |
. . . . . . . 8
|
91 | 89, 90 | nfan 1828 |
. . . . . . 7
|
92 | | nfv 1843 |
. . . . . . 7
|
93 | 91, 92 | nfan 1828 |
. . . . . 6
|
94 | | nfv 1843 |
. . . . . 6
|
95 | | nfv 1843 |
. . . . . . . . . . 11
|
96 | | nfra2 2946 |
. . . . . . . . . . 11
|
97 | 95, 96 | nfan 1828 |
. . . . . . . . . 10
|
98 | | nfv 1843 |
. . . . . . . . . 10
|
99 | 97, 98 | nfan 1828 |
. . . . . . . . 9
|
100 | | nfv 1843 |
. . . . . . . . 9
|
101 | 99, 100 | nfan 1828 |
. . . . . . . 8
|
102 | | nfv 1843 |
. . . . . . . 8
|
103 | | inss1 3833 |
. . . . . . . . . . . 12
|
104 | | simp3r 1090 |
. . . . . . . . . . . 12
|
105 | 103, 104 | syl5ss 3614 |
. . . . . . . . . . 11
|
106 | | inss2 3834 |
. . . . . . . . . . . 12
|
107 | 106 | a1i 11 |
. . . . . . . . . . 11
|
108 | 105, 107 | ssind 3837 |
. . . . . . . . . 10
|
109 | | simpllr 799 |
. . . . . . . . . . . 12
|
110 | 109 | 3ad2ant1 1082 |
. . . . . . . . . . 11
|
111 | | simp1r 1086 |
. . . . . . . . . . . 12
|
112 | | simp2 1062 |
. . . . . . . . . . . 12
|
113 | 111, 112 | jca 554 |
. . . . . . . . . . 11
|
114 | | simp3l 1089 |
. . . . . . . . . . 11
|
115 | | rsp2 2936 |
. . . . . . . . . . 11
|
116 | 110, 113,
114, 115 | syl3c 66 |
. . . . . . . . . 10
|
117 | | ssn0 3976 |
. . . . . . . . . 10
|
118 | 108, 116,
117 | syl2anc 693 |
. . . . . . . . 9
|
119 | 118 | 3exp 1264 |
. . . . . . . 8
|
120 | 101, 102,
119 | rexlimd 3026 |
. . . . . . 7
|
121 | 120 | ex 450 |
. . . . . 6
|
122 | 93, 94, 121 | rexlimd 3026 |
. . . . 5
|
123 | 88, 122 | mpd 15 |
. . . 4
|
124 | 123 | ralrimiva 2966 |
. . 3
|
125 | 38, 124 | impbida 877 |
. 2
|
126 | 10, 125 | bitrd 268 |
1
|