Step | Hyp | Ref
| Expression |
1 | | xmetxp.p |
. . 3
|
2 | | xmetxp.1 |
. . 3
|
3 | | xmetxp.2 |
. . 3
|
4 | | xmettx.j |
. . 3
|
5 | | xmettx.k |
. . 3
|
6 | | xmettx.l |
. . 3
|
7 | 1, 2, 3, 4, 5, 6 | xmettxlem 12979 |
. 2
|
8 | | eqid 2157 |
. . . . . . . . . . . 12
|
9 | 8 | elrnmpog 5935 |
. . . . . . . . . . 11
|
10 | 9 | elv 2716 |
. . . . . . . . . 10
|
11 | 10 | biimpi 119 |
. . . . . . . . 9
|
12 | 11 | adantl 275 |
. . . . . . . 8
|
13 | | xpeq1 4602 |
. . . . . . . . . 10
|
14 | 13 | eqeq2d 2169 |
. . . . . . . . 9
|
15 | | xpeq2 4603 |
. . . . . . . . . 10
|
16 | 15 | eqeq2d 2169 |
. . . . . . . . 9
|
17 | 14, 16 | cbvrex2v 2692 |
. . . . . . . 8
|
18 | 12, 17 | sylib 121 |
. . . . . . 7
|
19 | | simpr 109 |
. . . . . . . . . 10
|
20 | | simplll 523 |
. . . . . . . . . . 11
|
21 | | simplrl 525 |
. . . . . . . . . . 11
|
22 | | simplrr 526 |
. . . . . . . . . . 11
|
23 | 4 | mopntopon 12913 |
. . . . . . . . . . . . . . . . . 18
TopOn |
24 | 2, 23 | syl 14 |
. . . . . . . . . . . . . . . . 17
TopOn |
25 | 24 | adantr 274 |
. . . . . . . . . . . . . . . 16
TopOn |
26 | | simprl 521 |
. . . . . . . . . . . . . . . 16
|
27 | | toponss 12494 |
. . . . . . . . . . . . . . . 16
TopOn |
28 | 25, 26, 27 | syl2anc 409 |
. . . . . . . . . . . . . . 15
|
29 | 5 | mopntopon 12913 |
. . . . . . . . . . . . . . . . . 18
TopOn |
30 | 3, 29 | syl 14 |
. . . . . . . . . . . . . . . . 17
TopOn |
31 | 30 | adantr 274 |
. . . . . . . . . . . . . . . 16
TopOn |
32 | | simprr 522 |
. . . . . . . . . . . . . . . 16
|
33 | | toponss 12494 |
. . . . . . . . . . . . . . . 16
TopOn |
34 | 31, 32, 33 | syl2anc 409 |
. . . . . . . . . . . . . . 15
|
35 | | xpss12 4695 |
. . . . . . . . . . . . . . 15
|
36 | 28, 34, 35 | syl2anc 409 |
. . . . . . . . . . . . . 14
|
37 | 1, 2, 3 | xmetxp 12977 |
. . . . . . . . . . . . . . . 16
|
38 | | unirnbl 12893 |
. . . . . . . . . . . . . . . 16
|
39 | 37, 38 | syl 14 |
. . . . . . . . . . . . . . 15
|
40 | 39 | adantr 274 |
. . . . . . . . . . . . . 14
|
41 | 36, 40 | sseqtrrd 3167 |
. . . . . . . . . . . . 13
|
42 | 2 | ad2antrr 480 |
. . . . . . . . . . . . . . . 16
|
43 | | simplrl 525 |
. . . . . . . . . . . . . . . 16
|
44 | | xp1st 6115 |
. . . . . . . . . . . . . . . . 17
|
45 | 44 | adantl 275 |
. . . . . . . . . . . . . . . 16
|
46 | 4 | mopni2 12953 |
. . . . . . . . . . . . . . . 16
|
47 | 42, 43, 45, 46 | syl3anc 1220 |
. . . . . . . . . . . . . . 15
|
48 | 3 | ad2antrr 480 |
. . . . . . . . . . . . . . . . . 18
|
49 | | simplrr 526 |
. . . . . . . . . . . . . . . . . 18
|
50 | | xp2nd 6116 |
. . . . . . . . . . . . . . . . . . 19
|
51 | 50 | adantl 275 |
. . . . . . . . . . . . . . . . . 18
|
52 | 5 | mopni2 12953 |
. . . . . . . . . . . . . . . . . 18
|
53 | 48, 49, 51, 52 | syl3anc 1220 |
. . . . . . . . . . . . . . . . 17
|
54 | 53 | adantr 274 |
. . . . . . . . . . . . . . . 16
|
55 | | blf 12880 |
. . . . . . . . . . . . . . . . . . . . 21
|
56 | 37, 55 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
|
57 | 56 | ffnd 5322 |
. . . . . . . . . . . . . . . . . . 19
|
58 | 57 | ad4antr 486 |
. . . . . . . . . . . . . . . . . 18
|
59 | 36 | sselda 3128 |
. . . . . . . . . . . . . . . . . . 19
|
60 | 59 | ad2antrr 480 |
. . . . . . . . . . . . . . . . . 18
|
61 | | rpxr 9574 |
. . . . . . . . . . . . . . . . . . . . 21
|
62 | 61 | ad2antrl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
63 | 62 | adantr 274 |
. . . . . . . . . . . . . . . . . . 19
|
64 | | rpxr 9574 |
. . . . . . . . . . . . . . . . . . . 20
|
65 | 64 | ad2antrl 482 |
. . . . . . . . . . . . . . . . . . 19
|
66 | | xrmincl 11174 |
. . . . . . . . . . . . . . . . . . 19
inf |
67 | 63, 65, 66 | syl2anc 409 |
. . . . . . . . . . . . . . . . . 18
inf
|
68 | | fnovrn 5970 |
. . . . . . . . . . . . . . . . . 18
inf inf |
69 | 58, 60, 67, 68 | syl3anc 1220 |
. . . . . . . . . . . . . . . . 17
inf |
70 | | eleq2 2221 |
. . . . . . . . . . . . . . . . . . 19
inf
inf |
71 | | sseq1 3151 |
. . . . . . . . . . . . . . . . . . 19
inf
inf
|
72 | 70, 71 | anbi12d 465 |
. . . . . . . . . . . . . . . . . 18
inf
inf
inf
|
73 | 72 | adantl 275 |
. . . . . . . . . . . . . . . . 17
inf
inf
inf
|
74 | 37 | ad4antr 486 |
. . . . . . . . . . . . . . . . . . 19
|
75 | | simplrl 525 |
. . . . . . . . . . . . . . . . . . . 20
|
76 | | simprl 521 |
. . . . . . . . . . . . . . . . . . . 20
|
77 | | xrminrpcl 11182 |
. . . . . . . . . . . . . . . . . . . 20
inf |
78 | 75, 76, 77 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . 19
inf
|
79 | | blcntr 12886 |
. . . . . . . . . . . . . . . . . . 19
inf inf |
80 | 74, 60, 78, 79 | syl3anc 1220 |
. . . . . . . . . . . . . . . . . 18
inf |
81 | 42 | ad2antrr 480 |
. . . . . . . . . . . . . . . . . . . 20
|
82 | 48 | ad2antrr 480 |
. . . . . . . . . . . . . . . . . . . 20
|
83 | 1, 81, 82, 67, 60 | xmetxpbl 12978 |
. . . . . . . . . . . . . . . . . . 19
inf inf inf |
84 | 28 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
85 | 84, 45 | sseldd 3129 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
86 | 85 | ad2antrr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
|
87 | | xrmin1inf 11175 |
. . . . . . . . . . . . . . . . . . . . . . 23
inf |
88 | 63, 65, 87 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . . . . 22
inf
|
89 | | ssbl 12896 |
. . . . . . . . . . . . . . . . . . . . . 22
inf
inf
inf |
90 | 81, 86, 67, 63, 88, 89 | syl221anc 1231 |
. . . . . . . . . . . . . . . . . . . . 21
inf |
91 | | simplrr 526 |
. . . . . . . . . . . . . . . . . . . . 21
|
92 | 90, 91 | sstrd 3138 |
. . . . . . . . . . . . . . . . . . . 20
inf |
93 | 34 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
94 | 93, 51 | sseldd 3129 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
95 | 94 | ad2antrr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
|
96 | | xrmin2inf 11176 |
. . . . . . . . . . . . . . . . . . . . . . 23
inf |
97 | 63, 65, 96 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . . . . 22
inf
|
98 | | ssbl 12896 |
. . . . . . . . . . . . . . . . . . . . . 22
inf
inf
inf |
99 | 82, 95, 67, 65, 97, 98 | syl221anc 1231 |
. . . . . . . . . . . . . . . . . . . . 21
inf |
100 | | simprr 522 |
. . . . . . . . . . . . . . . . . . . . 21
|
101 | 99, 100 | sstrd 3138 |
. . . . . . . . . . . . . . . . . . . 20
inf |
102 | | xpss12 4695 |
. . . . . . . . . . . . . . . . . . . 20
inf inf
inf inf |
103 | 92, 101, 102 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . 19
inf inf |
104 | 83, 103 | eqsstrd 3164 |
. . . . . . . . . . . . . . . . . 18
inf
|
105 | 80, 104 | jca 304 |
. . . . . . . . . . . . . . . . 17
inf inf
|
106 | 69, 73, 105 | rspcedvd 2822 |
. . . . . . . . . . . . . . . 16
|
107 | 54, 106 | rexlimddv 2579 |
. . . . . . . . . . . . . . 15
|
108 | 47, 107 | rexlimddv 2579 |
. . . . . . . . . . . . . 14
|
109 | 108 | ralrimiva 2530 |
. . . . . . . . . . . . 13
|
110 | 41, 109 | jca 304 |
. . . . . . . . . . . 12
|
111 | | blex 12857 |
. . . . . . . . . . . . . . 15
|
112 | 37, 111 | syl 14 |
. . . . . . . . . . . . . 14
|
113 | 112 | adantr 274 |
. . . . . . . . . . . . 13
|
114 | | rnexg 4853 |
. . . . . . . . . . . . 13
|
115 | | eltg2 12523 |
. . . . . . . . . . . . 13
|
116 | 113, 114,
115 | 3syl 17 |
. . . . . . . . . . . 12
|
117 | 110, 116 | mpbird 166 |
. . . . . . . . . . 11
|
118 | 20, 21, 22, 117 | syl12anc 1218 |
. . . . . . . . . 10
|
119 | 19, 118 | eqeltrd 2234 |
. . . . . . . . 9
|
120 | 119 | ex 114 |
. . . . . . . 8
|
121 | 120 | rexlimdvva 2582 |
. . . . . . 7
|
122 | 18, 121 | mpd 13 |
. . . . . 6
|
123 | 122 | ex 114 |
. . . . 5
|
124 | 123 | ssrdv 3134 |
. . . 4
|
125 | 4 | mopntop 12914 |
. . . . . . . 8
|
126 | 2, 125 | syl 14 |
. . . . . . 7
|
127 | 5 | mopntop 12914 |
. . . . . . . 8
|
128 | 3, 127 | syl 14 |
. . . . . . 7
|
129 | | mpoexga 6162 |
. . . . . . 7
|
130 | 126, 128,
129 | syl2anc 409 |
. . . . . 6
|
131 | | rnexg 4853 |
. . . . . 6
|
132 | 130, 131 | syl 14 |
. . . . 5
|
133 | 37, 111, 114 | 3syl 17 |
. . . . 5
|
134 | | tgss3 12548 |
. . . . 5
|
135 | 132, 133,
134 | syl2anc 409 |
. . . 4
|
136 | 124, 135 | mpbird 166 |
. . 3
|
137 | | eqid 2157 |
. . . . 5
|
138 | 137 | txval 12725 |
. . . 4
|
139 | 126, 128,
138 | syl2anc 409 |
. . 3
|
140 | 6 | mopnval 12912 |
. . . 4
|
141 | 37, 140 | syl 14 |
. . 3
|
142 | 136, 139,
141 | 3sstr4d 3173 |
. 2
|
143 | 7, 142 | eqssd 3145 |
1
|