Step | Hyp | Ref
| Expression |
1 | | vex 3203 |
. . . . . . . 8
|
2 | | vex 3203 |
. . . . . . . 8
|
3 | 1, 2 | xpex 6962 |
. . . . . . 7
|
4 | 3 | rgen2w 2925 |
. . . . . 6
|
5 | | eqid 2622 |
. . . . . . 7
|
6 | | eleq2 2690 |
. . . . . . . 8
|
7 | | sseq2 3627 |
. . . . . . . . 9
|
8 | 7 | rexbidv 3052 |
. . . . . . . 8
|
9 | 6, 8 | imbi12d 334 |
. . . . . . 7
|
10 | 5, 9 | ralrnmpt2 6775 |
. . . . . 6
|
11 | 4, 10 | ax-mp 5 |
. . . . 5
|
12 | | opelxp 5146 |
. . . . . . . . . . . . . . . 16
|
13 | | ancom 466 |
. . . . . . . . . . . . . . . 16
|
14 | 12, 13 | bitri 264 |
. . . . . . . . . . . . . . 15
|
15 | 14 | a1i 11 |
. . . . . . . . . . . . . 14
|
16 | | r19.40 3088 |
. . . . . . . . . . . . . . . . 17
|
17 | | raleq 3138 |
. . . . . . . . . . . . . . . . . . 19
|
18 | 17 | cbvrexv 3172 |
. . . . . . . . . . . . . . . . . 18
|
19 | | raleq 3138 |
. . . . . . . . . . . . . . . . . . 19
|
20 | 19 | cbvrexv 3172 |
. . . . . . . . . . . . . . . . . 18
|
21 | 18, 20 | anbi12i 733 |
. . . . . . . . . . . . . . . . 17
|
22 | 16, 21 | sylib 208 |
. . . . . . . . . . . . . . . 16
|
23 | | reeanv 3107 |
. . . . . . . . . . . . . . . . 17
|
24 | | txflf.l |
. . . . . . . . . . . . . . . . . . . . 21
|
25 | | filin 21658 |
. . . . . . . . . . . . . . . . . . . . . 22
|
26 | 25 | 3expb 1266 |
. . . . . . . . . . . . . . . . . . . . 21
|
27 | 24, 26 | sylan 488 |
. . . . . . . . . . . . . . . . . . . 20
|
28 | | inss1 3833 |
. . . . . . . . . . . . . . . . . . . . . 22
|
29 | | ssralv 3666 |
. . . . . . . . . . . . . . . . . . . . . 22
|
30 | 28, 29 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
|
31 | | inss2 3834 |
. . . . . . . . . . . . . . . . . . . . . 22
|
32 | | ssralv 3666 |
. . . . . . . . . . . . . . . . . . . . . 22
|
33 | 31, 32 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
|
34 | 30, 33 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . 20
|
35 | | raleq 3138 |
. . . . . . . . . . . . . . . . . . . . . 22
|
36 | | raleq 3138 |
. . . . . . . . . . . . . . . . . . . . . 22
|
37 | 35, 36 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . 21
|
38 | 37 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . 20
|
39 | 27, 34, 38 | syl2an 494 |
. . . . . . . . . . . . . . . . . . 19
|
40 | 39 | ex 450 |
. . . . . . . . . . . . . . . . . 18
|
41 | 40 | rexlimdvva 3038 |
. . . . . . . . . . . . . . . . 17
|
42 | 23, 41 | syl5bir 233 |
. . . . . . . . . . . . . . . 16
|
43 | 22, 42 | impbid2 216 |
. . . . . . . . . . . . . . 15
|
44 | | df-ima 5127 |
. . . . . . . . . . . . . . . . . . 19
|
45 | | filelss 21656 |
. . . . . . . . . . . . . . . . . . . . . 22
|
46 | 24, 45 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . 21
|
47 | | txflf.h |
. . . . . . . . . . . . . . . . . . . . . . 23
|
48 | 47 | reseq1i 5392 |
. . . . . . . . . . . . . . . . . . . . . 22
|
49 | | resmpt 5449 |
. . . . . . . . . . . . . . . . . . . . . 22
|
50 | 48, 49 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . 21
|
51 | 46, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
52 | 51 | rneqd 5353 |
. . . . . . . . . . . . . . . . . . 19
|
53 | 44, 52 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . 18
|
54 | 53 | sseq1d 3632 |
. . . . . . . . . . . . . . . . 17
|
55 | | opelxp 5146 |
. . . . . . . . . . . . . . . . . . 19
|
56 | 55 | ralbii 2980 |
. . . . . . . . . . . . . . . . . 18
|
57 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
|
58 | 57 | fmpt 6381 |
. . . . . . . . . . . . . . . . . . 19
|
59 | | opex 4932 |
. . . . . . . . . . . . . . . . . . . . 21
|
60 | 59, 57 | fnmpti 6022 |
. . . . . . . . . . . . . . . . . . . 20
|
61 | | df-f 5892 |
. . . . . . . . . . . . . . . . . . . 20
|
62 | 60, 61 | mpbiran 953 |
. . . . . . . . . . . . . . . . . . 19
|
63 | 58, 62 | bitri 264 |
. . . . . . . . . . . . . . . . . 18
|
64 | | r19.26 3064 |
. . . . . . . . . . . . . . . . . 18
|
65 | 56, 63, 64 | 3bitr3i 290 |
. . . . . . . . . . . . . . . . 17
|
66 | 54, 65 | syl6bb 276 |
. . . . . . . . . . . . . . . 16
|
67 | 66 | rexbidva 3049 |
. . . . . . . . . . . . . . 15
|
68 | | txflf.f |
. . . . . . . . . . . . . . . . . . . 20
|
69 | 68 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
70 | | ffun 6048 |
. . . . . . . . . . . . . . . . . . 19
|
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
72 | | filelss 21656 |
. . . . . . . . . . . . . . . . . . . 20
|
73 | 24, 72 | sylan 488 |
. . . . . . . . . . . . . . . . . . 19
|
74 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . 20
|
75 | 69, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
76 | 73, 75 | sseqtr4d 3642 |
. . . . . . . . . . . . . . . . . 18
|
77 | | funimass4 6247 |
. . . . . . . . . . . . . . . . . 18
|
78 | 71, 76, 77 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
79 | 78 | rexbidva 3049 |
. . . . . . . . . . . . . . . 16
|
80 | | txflf.g |
. . . . . . . . . . . . . . . . . . . 20
|
81 | 80 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
82 | | ffun 6048 |
. . . . . . . . . . . . . . . . . . 19
|
83 | 81, 82 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
84 | | filelss 21656 |
. . . . . . . . . . . . . . . . . . . 20
|
85 | 24, 84 | sylan 488 |
. . . . . . . . . . . . . . . . . . 19
|
86 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . 20
|
87 | 81, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
88 | 85, 87 | sseqtr4d 3642 |
. . . . . . . . . . . . . . . . . 18
|
89 | | funimass4 6247 |
. . . . . . . . . . . . . . . . . 18
|
90 | 83, 88, 89 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
91 | 90 | rexbidva 3049 |
. . . . . . . . . . . . . . . 16
|
92 | 79, 91 | anbi12d 747 |
. . . . . . . . . . . . . . 15
|
93 | 43, 67, 92 | 3bitr4d 300 |
. . . . . . . . . . . . . 14
|
94 | 15, 93 | imbi12d 334 |
. . . . . . . . . . . . 13
|
95 | | impexp 462 |
. . . . . . . . . . . . 13
|
96 | 94, 95 | syl6bb 276 |
. . . . . . . . . . . 12
|
97 | 96 | ralbidv 2986 |
. . . . . . . . . . 11
|
98 | | eleq2 2690 |
. . . . . . . . . . . . 13
|
99 | 98 | ralrab 3368 |
. . . . . . . . . . . 12
|
100 | | r19.21v 2960 |
. . . . . . . . . . . 12
|
101 | 99, 100 | bitr3i 266 |
. . . . . . . . . . 11
|
102 | 97, 101 | syl6bb 276 |
. . . . . . . . . 10
|
103 | 102 | ralbidv 2986 |
. . . . . . . . 9
|
104 | | eleq2 2690 |
. . . . . . . . . 10
|
105 | 104 | ralrab 3368 |
. . . . . . . . 9
|
106 | 103, 105 | syl6bbr 278 |
. . . . . . . 8
|
107 | 106 | adantr 481 |
. . . . . . 7
|
108 | | txflf.j |
. . . . . . . . . . 11
TopOn |
109 | | toponmax 20730 |
. . . . . . . . . . 11
TopOn
|
110 | 108, 109 | syl 17 |
. . . . . . . . . 10
|
111 | | eleq2 2690 |
. . . . . . . . . . . 12
|
112 | 111 | rspcev 3309 |
. . . . . . . . . . 11
|
113 | | rabn0 3958 |
. . . . . . . . . . 11
|
114 | 112, 113 | sylibr 224 |
. . . . . . . . . 10
|
115 | 110, 114 | sylan 488 |
. . . . . . . . 9
|
116 | | txflf.k |
. . . . . . . . . . 11
TopOn |
117 | | toponmax 20730 |
. . . . . . . . . . 11
TopOn
|
118 | 116, 117 | syl 17 |
. . . . . . . . . 10
|
119 | | eleq2 2690 |
. . . . . . . . . . . 12
|
120 | 119 | rspcev 3309 |
. . . . . . . . . . 11
|
121 | | rabn0 3958 |
. . . . . . . . . . 11
|
122 | 120, 121 | sylibr 224 |
. . . . . . . . . 10
|
123 | 118, 122 | sylan 488 |
. . . . . . . . 9
|
124 | 115, 123 | anim12dan 882 |
. . . . . . . 8
|
125 | | r19.28zv 4066 |
. . . . . . . . . 10
|
126 | 125 | ralbidv 2986 |
. . . . . . . . 9
|
127 | | r19.27zv 4071 |
. . . . . . . . 9
|
128 | 126, 127 | sylan9bbr 737 |
. . . . . . . 8
|
129 | 124, 128 | syl 17 |
. . . . . . 7
|
130 | 107, 129 | bitrd 268 |
. . . . . 6
|
131 | 104 | ralrab 3368 |
. . . . . . 7
|
132 | 98 | ralrab 3368 |
. . . . . . 7
|
133 | 131, 132 | anbi12i 733 |
. . . . . 6
|
134 | 130, 133 | syl6bb 276 |
. . . . 5
|
135 | 11, 134 | syl5bb 272 |
. . . 4
|
136 | 135 | pm5.32da 673 |
. . 3
|
137 | | opelxp 5146 |
. . . 4
|
138 | 137 | anbi1i 731 |
. . 3
|
139 | | an4 865 |
. . 3
|
140 | 136, 138,
139 | 3bitr4g 303 |
. 2
|
141 | | eqid 2622 |
. . . . . . . 8
|
142 | 141 | txval 21367 |
. . . . . . 7
TopOn TopOn
|
143 | 108, 116,
142 | syl2anc 693 |
. . . . . 6
|
144 | 143 | oveq1d 6665 |
. . . . 5
|
145 | 144 | fveq1d 6193 |
. . . 4
|
146 | 145 | eleq2d 2687 |
. . 3
|
147 | | txtopon 21394 |
. . . . . 6
TopOn TopOn
TopOn |
148 | 108, 116,
147 | syl2anc 693 |
. . . . 5
TopOn
|
149 | 143, 148 | eqeltrrd 2702 |
. . . 4
TopOn
|
150 | 68 | ffvelrnda 6359 |
. . . . . 6
|
151 | 80 | ffvelrnda 6359 |
. . . . . 6
|
152 | | opelxpi 5148 |
. . . . . 6
|
153 | 150, 151,
152 | syl2anc 693 |
. . . . 5
|
154 | 153, 47 | fmptd 6385 |
. . . 4
|
155 | | eqid 2622 |
. . . . 5
|
156 | 155 | flftg 21800 |
. . . 4
TopOn
|
157 | 149, 24, 154, 156 | syl3anc 1326 |
. . 3
|
158 | 146, 157 | bitrd 268 |
. 2
|
159 | | isflf 21797 |
. . . 4
TopOn
|
160 | 108, 24, 68, 159 | syl3anc 1326 |
. . 3
|
161 | | isflf 21797 |
. . . 4
TopOn
|
162 | 116, 24, 80, 161 | syl3anc 1326 |
. . 3
|
163 | 160, 162 | anbi12d 747 |
. 2
|
164 | 140, 158,
163 | 3bitr4d 300 |
1
|