Step | Hyp | Ref
| Expression |
1 | | r19.27v 3070 |
. . . . . . . 8
|
2 | | r19.28v 3071 |
. . . . . . . . 9
|
3 | 2 | ralimi 2952 |
. . . . . . . 8
|
4 | 1, 3 | syl 17 |
. . . . . . 7
|
5 | | simprl 794 |
. . . . . . . . . . . . . . 15
|
6 | | txlm.j |
. . . . . . . . . . . . . . . . . 18
TopOn |
7 | | topontop 20718 |
. . . . . . . . . . . . . . . . . 18
TopOn
|
8 | 6, 7 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
9 | | txlm.k |
. . . . . . . . . . . . . . . . . 18
TopOn |
10 | | topontop 20718 |
. . . . . . . . . . . . . . . . . 18
TopOn
|
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
12 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
|
13 | 12 | txval 21367 |
. . . . . . . . . . . . . . . . 17
|
14 | 8, 11, 13 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
15 | 14 | adantr 481 |
. . . . . . . . . . . . . . 15
|
16 | 5, 15 | eleqtrd 2703 |
. . . . . . . . . . . . . 14
|
17 | | simprr 796 |
. . . . . . . . . . . . . 14
|
18 | | tg2 20769 |
. . . . . . . . . . . . . 14
|
19 | 16, 17, 18 | syl2anc 693 |
. . . . . . . . . . . . 13
|
20 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
21 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
22 | 20, 21 | xpex 6962 |
. . . . . . . . . . . . . . 15
|
23 | 22 | rgen2w 2925 |
. . . . . . . . . . . . . 14
|
24 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
25 | | eleq2 2690 |
. . . . . . . . . . . . . . . 16
|
26 | | sseq1 3626 |
. . . . . . . . . . . . . . . 16
|
27 | 25, 26 | anbi12d 747 |
. . . . . . . . . . . . . . 15
|
28 | 24, 27 | rexrnmpt2 6776 |
. . . . . . . . . . . . . 14
|
29 | 23, 28 | ax-mp 5 |
. . . . . . . . . . . . 13
|
30 | 19, 29 | sylib 208 |
. . . . . . . . . . . 12
|
31 | 30 | ex 450 |
. . . . . . . . . . 11
|
32 | | r19.29 3072 |
. . . . . . . . . . . . 13
|
33 | | r19.29 3072 |
. . . . . . . . . . . . . . 15
|
34 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . 22
|
35 | | opelxp 5146 |
. . . . . . . . . . . . . . . . . . . . . 22
|
36 | 34, 35 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . 21
|
37 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . . . . . 22
|
38 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . . . . . 22
|
39 | 37, 38 | im2anan9 880 |
. . . . . . . . . . . . . . . . . . . . 21
|
40 | 36, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
41 | | txlm.z |
. . . . . . . . . . . . . . . . . . . . . 22
|
42 | 41 | rexanuz2 14089 |
. . . . . . . . . . . . . . . . . . . . 21
|
43 | 41 | uztrn2 11705 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
44 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
45 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
46 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
47 | 45, 46 | opeq12d 4410 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
48 | | txlm.h |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
49 | | opex 4932 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
50 | 47, 48, 49 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
51 | 50 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
52 | 44, 51 | syl5ibr 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
53 | 52 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
54 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
55 | 54 | sseld 3602 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
56 | 53, 55 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
57 | 43, 56 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
58 | 57 | anassrs 680 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
59 | 58 | ralimdva 2962 |
. . . . . . . . . . . . . . . . . . . . . 22
|
60 | 59 | reximdva 3017 |
. . . . . . . . . . . . . . . . . . . . 21
|
61 | 42, 60 | syl5bir 233 |
. . . . . . . . . . . . . . . . . . . 20
|
62 | 40, 61 | syld 47 |
. . . . . . . . . . . . . . . . . . 19
|
63 | 62 | ex 450 |
. . . . . . . . . . . . . . . . . 18
|
64 | 63 | com23 86 |
. . . . . . . . . . . . . . . . 17
|
65 | 64 | impd 447 |
. . . . . . . . . . . . . . . 16
|
66 | 65 | rexlimdva 3031 |
. . . . . . . . . . . . . . 15
|
67 | 33, 66 | syl5 34 |
. . . . . . . . . . . . . 14
|
68 | 67 | rexlimdva 3031 |
. . . . . . . . . . . . 13
|
69 | 32, 68 | syl5 34 |
. . . . . . . . . . . 12
|
70 | 69 | expcomd 454 |
. . . . . . . . . . 11
|
71 | 31, 70 | syld 47 |
. . . . . . . . . 10
|
72 | 71 | expdimp 453 |
. . . . . . . . 9
|
73 | 72 | com23 86 |
. . . . . . . 8
|
74 | 73 | ralrimdva 2969 |
. . . . . . 7
|
75 | 4, 74 | syl5 34 |
. . . . . 6
|
76 | 75 | adantr 481 |
. . . . 5
|
77 | 8 | adantr 481 |
. . . . . . . . . . . 12
|
78 | 11 | adantr 481 |
. . . . . . . . . . . 12
|
79 | | simprr 796 |
. . . . . . . . . . . 12
|
80 | | toponmax 20730 |
. . . . . . . . . . . . . 14
TopOn
|
81 | 9, 80 | syl 17 |
. . . . . . . . . . . . 13
|
82 | 81 | adantr 481 |
. . . . . . . . . . . 12
|
83 | | txopn 21405 |
. . . . . . . . . . . 12
|
84 | 77, 78, 79, 82, 83 | syl22anc 1327 |
. . . . . . . . . . 11
|
85 | | eleq2 2690 |
. . . . . . . . . . . . 13
|
86 | | eleq2 2690 |
. . . . . . . . . . . . . 14
|
87 | 86 | rexralbidv 3058 |
. . . . . . . . . . . . 13
|
88 | 85, 87 | imbi12d 334 |
. . . . . . . . . . . 12
|
89 | 88 | rspcv 3305 |
. . . . . . . . . . 11
|
90 | 84, 89 | syl 17 |
. . . . . . . . . 10
|
91 | | simprl 794 |
. . . . . . . . . . . . 13
|
92 | | opelxpi 5148 |
. . . . . . . . . . . . 13
|
93 | 91, 92 | sylan2 491 |
. . . . . . . . . . . 12
|
94 | 93 | expcom 451 |
. . . . . . . . . . 11
|
95 | 50 | eleq1d 2686 |
. . . . . . . . . . . . . . . 16
|
96 | | opelxp1 5150 |
. . . . . . . . . . . . . . . 16
|
97 | 95, 96 | syl6bi 243 |
. . . . . . . . . . . . . . 15
|
98 | 43, 97 | syl 17 |
. . . . . . . . . . . . . 14
|
99 | 98 | ralimdva 2962 |
. . . . . . . . . . . . 13
|
100 | 99 | reximia 3009 |
. . . . . . . . . . . 12
|
101 | 100 | a1i 11 |
. . . . . . . . . . 11
|
102 | 94, 101 | imim12d 81 |
. . . . . . . . . 10
|
103 | 90, 102 | syld 47 |
. . . . . . . . 9
|
104 | 103 | anassrs 680 |
. . . . . . . 8
|
105 | 104 | ralrimdva 2969 |
. . . . . . 7
|
106 | 105 | adantrl 752 |
. . . . . 6
|
107 | 8 | adantr 481 |
. . . . . . . . . . . 12
|
108 | 11 | adantr 481 |
. . . . . . . . . . . 12
|
109 | | toponmax 20730 |
. . . . . . . . . . . . . 14
TopOn
|
110 | 6, 109 | syl 17 |
. . . . . . . . . . . . 13
|
111 | 110 | adantr 481 |
. . . . . . . . . . . 12
|
112 | | simprr 796 |
. . . . . . . . . . . 12
|
113 | | txopn 21405 |
. . . . . . . . . . . 12
|
114 | 107, 108,
111, 112, 113 | syl22anc 1327 |
. . . . . . . . . . 11
|
115 | | eleq2 2690 |
. . . . . . . . . . . . 13
|
116 | | eleq2 2690 |
. . . . . . . . . . . . . 14
|
117 | 116 | rexralbidv 3058 |
. . . . . . . . . . . . 13
|
118 | 115, 117 | imbi12d 334 |
. . . . . . . . . . . 12
|
119 | 118 | rspcv 3305 |
. . . . . . . . . . 11
|
120 | 114, 119 | syl 17 |
. . . . . . . . . 10
|
121 | | opelxpi 5148 |
. . . . . . . . . . . . 13
|
122 | 121 | ex 450 |
. . . . . . . . . . . 12
|
123 | 122 | ad2antrl 764 |
. . . . . . . . . . 11
|
124 | 50 | eleq1d 2686 |
. . . . . . . . . . . . . . . 16
|
125 | | opelxp2 5151 |
. . . . . . . . . . . . . . . 16
|
126 | 124, 125 | syl6bi 243 |
. . . . . . . . . . . . . . 15
|
127 | 43, 126 | syl 17 |
. . . . . . . . . . . . . 14
|
128 | 127 | ralimdva 2962 |
. . . . . . . . . . . . 13
|
129 | 128 | reximia 3009 |
. . . . . . . . . . . 12
|
130 | 129 | a1i 11 |
. . . . . . . . . . 11
|
131 | 123, 130 | imim12d 81 |
. . . . . . . . . 10
|
132 | 120, 131 | syld 47 |
. . . . . . . . 9
|
133 | 132 | anassrs 680 |
. . . . . . . 8
|
134 | 133 | ralrimdva 2969 |
. . . . . . 7
|
135 | 134 | adantrr 753 |
. . . . . 6
|
136 | 106, 135 | jcad 555 |
. . . . 5
|
137 | 76, 136 | impbid 202 |
. . . 4
|
138 | 137 | pm5.32da 673 |
. . 3
|
139 | | opelxp 5146 |
. . . 4
|
140 | 139 | anbi1i 731 |
. . 3
|
141 | 138, 140 | syl6bbr 278 |
. 2
|
142 | | txlm.m |
. . . . 5
|
143 | | txlm.f |
. . . . 5
|
144 | | eqidd 2623 |
. . . . 5
|
145 | 6, 41, 142, 143, 144 | lmbrf 21064 |
. . . 4
|
146 | | txlm.g |
. . . . 5
|
147 | | eqidd 2623 |
. . . . 5
|
148 | 9, 41, 142, 146, 147 | lmbrf 21064 |
. . . 4
|
149 | 145, 148 | anbi12d 747 |
. . 3
|
150 | | an4 865 |
. . 3
|
151 | 149, 150 | syl6bb 276 |
. 2
|
152 | | txtopon 21394 |
. . . 4
TopOn TopOn
TopOn |
153 | 6, 9, 152 | syl2anc 693 |
. . 3
TopOn
|
154 | 143 | ffvelrnda 6359 |
. . . . 5
|
155 | 146 | ffvelrnda 6359 |
. . . . 5
|
156 | | opelxpi 5148 |
. . . . 5
|
157 | 154, 155,
156 | syl2anc 693 |
. . . 4
|
158 | 157, 48 | fmptd 6385 |
. . 3
|
159 | | eqidd 2623 |
. . 3
|
160 | 153, 41, 142, 158, 159 | lmbrf 21064 |
. 2
|
161 | 141, 151,
160 | 3bitr4d 300 |
1
|