Step | Hyp | Ref
| Expression |
1 | | methaus.1 |
. . . . 5
|
2 | 1 | mopntop 22245 |
. . . 4
|
3 | 2 | adantr 481 |
. . 3
|
4 | | simpll 790 |
. . . . . . 7
|
5 | | simplr1 1103 |
. . . . . . . 8
|
6 | | simprr 796 |
. . . . . . . 8
|
7 | 5, 6 | sseldd 3604 |
. . . . . . 7
|
8 | | simprl 794 |
. . . . . . . . . 10
|
9 | 8 | nnrpd 11870 |
. . . . . . . . 9
|
10 | 9 | rpreccld 11882 |
. . . . . . . 8
|
11 | 10 | rpxrd 11873 |
. . . . . . 7
|
12 | 1 | blopn 22305 |
. . . . . . 7
|
13 | 4, 7, 11, 12 | syl3anc 1326 |
. . . . . 6
|
14 | 13 | ralrimivva 2971 |
. . . . 5
|
15 | | eqid 2622 |
. . . . . 6
|
16 | 15 | fmpt2 7237 |
. . . . 5
|
17 | 14, 16 | sylib 208 |
. . . 4
|
18 | | frn 6053 |
. . . 4
|
19 | 17, 18 | syl 17 |
. . 3
|
20 | | simpll 790 |
. . . . . 6
|
21 | | simprl 794 |
. . . . . 6
|
22 | | simprr 796 |
. . . . . 6
|
23 | 1 | mopni2 22298 |
. . . . . 6
|
24 | 20, 21, 22, 23 | syl3anc 1326 |
. . . . 5
|
25 | | simprl 794 |
. . . . . . . 8
|
26 | 25 | rphalfcld 11884 |
. . . . . . 7
|
27 | | elrp 11834 |
. . . . . . . 8
|
28 | | nnrecl 11290 |
. . . . . . . 8
|
29 | 27, 28 | sylbi 207 |
. . . . . . 7
|
30 | 26, 29 | syl 17 |
. . . . . 6
|
31 | 3 | ad2antrr 762 |
. . . . . . . . . 10
|
32 | | simpr1 1067 |
. . . . . . . . . . . 12
|
33 | 32 | ad2antrr 762 |
. . . . . . . . . . 11
|
34 | 1 | mopnuni 22246 |
. . . . . . . . . . . 12
|
35 | 34 | ad3antrrr 766 |
. . . . . . . . . . 11
|
36 | 33, 35 | sseqtrd 3641 |
. . . . . . . . . 10
|
37 | | simplrr 801 |
. . . . . . . . . . . . 13
|
38 | | simplrl 800 |
. . . . . . . . . . . . 13
|
39 | | elunii 4441 |
. . . . . . . . . . . . 13
|
40 | 37, 38, 39 | syl2anc 693 |
. . . . . . . . . . . 12
|
41 | 40, 35 | eleqtrrd 2704 |
. . . . . . . . . . 11
|
42 | | simpr3 1069 |
. . . . . . . . . . . 12
|
43 | 42 | ad2antrr 762 |
. . . . . . . . . . 11
|
44 | 41, 43 | eleqtrrd 2704 |
. . . . . . . . . 10
|
45 | 20 | adantr 481 |
. . . . . . . . . . 11
|
46 | | simprrl 804 |
. . . . . . . . . . . . . 14
|
47 | 46 | nnrpd 11870 |
. . . . . . . . . . . . 13
|
48 | 47 | rpreccld 11882 |
. . . . . . . . . . . 12
|
49 | 48 | rpxrd 11873 |
. . . . . . . . . . 11
|
50 | 1 | blopn 22305 |
. . . . . . . . . . 11
|
51 | 45, 41, 49, 50 | syl3anc 1326 |
. . . . . . . . . 10
|
52 | | blcntr 22218 |
. . . . . . . . . . 11
|
53 | 45, 41, 48, 52 | syl3anc 1326 |
. . . . . . . . . 10
|
54 | | eqid 2622 |
. . . . . . . . . . 11
|
55 | 54 | clsndisj 20879 |
. . . . . . . . . 10
|
56 | 31, 36, 44, 51, 53, 55 | syl32anc 1334 |
. . . . . . . . 9
|
57 | | n0 3931 |
. . . . . . . . 9
|
58 | 56, 57 | sylib 208 |
. . . . . . . 8
|
59 | 46 | adantr 481 |
. . . . . . . . . . 11
|
60 | | inss2 3834 |
. . . . . . . . . . . 12
|
61 | | simpr 477 |
. . . . . . . . . . . 12
|
62 | 60, 61 | sseldi 3601 |
. . . . . . . . . . 11
|
63 | | eqidd 2623 |
. . . . . . . . . . 11
|
64 | | oveq2 6658 |
. . . . . . . . . . . . . 14
|
65 | 64 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
66 | 65 | eqeq2d 2632 |
. . . . . . . . . . . 12
|
67 | | oveq1 6657 |
. . . . . . . . . . . . 13
|
68 | 67 | eqeq2d 2632 |
. . . . . . . . . . . 12
|
69 | 66, 68 | rspc2ev 3324 |
. . . . . . . . . . 11
|
70 | 59, 62, 63, 69 | syl3anc 1326 |
. . . . . . . . . 10
|
71 | | ovex 6678 |
. . . . . . . . . . 11
|
72 | | eqeq1 2626 |
. . . . . . . . . . . 12
|
73 | 72 | 2rexbidv 3057 |
. . . . . . . . . . 11
|
74 | 15 | rnmpt2 6770 |
. . . . . . . . . . 11
|
75 | 71, 73, 74 | elab2 3354 |
. . . . . . . . . 10
|
76 | 70, 75 | sylibr 224 |
. . . . . . . . 9
|
77 | | inss1 3833 |
. . . . . . . . . . 11
|
78 | 77, 61 | sseldi 3601 |
. . . . . . . . . 10
|
79 | 45 | adantr 481 |
. . . . . . . . . . 11
|
80 | 49 | adantr 481 |
. . . . . . . . . . 11
|
81 | 41 | adantr 481 |
. . . . . . . . . . 11
|
82 | 33 | adantr 481 |
. . . . . . . . . . . 12
|
83 | 82, 62 | sseldd 3604 |
. . . . . . . . . . 11
|
84 | | blcom 22199 |
. . . . . . . . . . 11
|
85 | 79, 80, 81, 83, 84 | syl22anc 1327 |
. . . . . . . . . 10
|
86 | 78, 85 | mpbid 222 |
. . . . . . . . 9
|
87 | | simprll 802 |
. . . . . . . . . . . . . 14
|
88 | 87 | adantr 481 |
. . . . . . . . . . . . 13
|
89 | 88 | rphalfcld 11884 |
. . . . . . . . . . . 12
|
90 | 89 | rpxrd 11873 |
. . . . . . . . . . 11
|
91 | | simprrr 805 |
. . . . . . . . . . . . 13
|
92 | 87 | rphalfcld 11884 |
. . . . . . . . . . . . . 14
|
93 | | rpre 11839 |
. . . . . . . . . . . . . . 15
|
94 | | rpre 11839 |
. . . . . . . . . . . . . . 15
|
95 | | ltle 10126 |
. . . . . . . . . . . . . . 15
|
96 | 93, 94, 95 | syl2an 494 |
. . . . . . . . . . . . . 14
|
97 | 48, 92, 96 | syl2anc 693 |
. . . . . . . . . . . . 13
|
98 | 91, 97 | mpd 15 |
. . . . . . . . . . . 12
|
99 | 98 | adantr 481 |
. . . . . . . . . . 11
|
100 | | ssbl 22228 |
. . . . . . . . . . 11
|
101 | 79, 83, 80, 90, 99, 100 | syl221anc 1337 |
. . . . . . . . . 10
|
102 | 88 | rpred 11872 |
. . . . . . . . . . . 12
|
103 | 101, 86 | sseldd 3604 |
. . . . . . . . . . . 12
|
104 | | blhalf 22210 |
. . . . . . . . . . . 12
|
105 | 79, 83, 102, 103, 104 | syl22anc 1327 |
. . . . . . . . . . 11
|
106 | | simprlr 803 |
. . . . . . . . . . . 12
|
107 | 106 | adantr 481 |
. . . . . . . . . . 11
|
108 | 105, 107 | sstrd 3613 |
. . . . . . . . . 10
|
109 | 101, 108 | sstrd 3613 |
. . . . . . . . 9
|
110 | | eleq2 2690 |
. . . . . . . . . . 11
|
111 | | sseq1 3626 |
. . . . . . . . . . 11
|
112 | 110, 111 | anbi12d 747 |
. . . . . . . . . 10
|
113 | 112 | rspcev 3309 |
. . . . . . . . 9
|
114 | 76, 86, 109, 113 | syl12anc 1324 |
. . . . . . . 8
|
115 | 58, 114 | exlimddv 1863 |
. . . . . . 7
|
116 | 115 | anassrs 680 |
. . . . . 6
|
117 | 30, 116 | rexlimddv 3035 |
. . . . 5
|
118 | 24, 117 | rexlimddv 3035 |
. . . 4
|
119 | 118 | ralrimivva 2971 |
. . 3
|
120 | | basgen2 20793 |
. . 3
|
121 | 3, 19, 119, 120 | syl3anc 1326 |
. 2
|
122 | 121, 3 | eqeltrd 2701 |
. . . 4
|
123 | | tgclb 20774 |
. . . 4
|
124 | 122, 123 | sylibr 224 |
. . 3
|
125 | | omelon 8543 |
. . . . . 6
|
126 | | simpr2 1068 |
. . . . . . . 8
|
127 | | nnex 11026 |
. . . . . . . . 9
|
128 | 127 | xpdom2 8055 |
. . . . . . . 8
|
129 | 126, 128 | syl 17 |
. . . . . . 7
|
130 | | nnenom 12779 |
. . . . . . . . 9
|
131 | | omex 8540 |
. . . . . . . . . 10
|
132 | 131 | enref 7988 |
. . . . . . . . 9
|
133 | | xpen 8123 |
. . . . . . . . 9
|
134 | 130, 132,
133 | mp2an 708 |
. . . . . . . 8
|
135 | | xpomen 8838 |
. . . . . . . 8
|
136 | 134, 135 | entri 8010 |
. . . . . . 7
|
137 | | domentr 8015 |
. . . . . . 7
|
138 | 129, 136,
137 | sylancl 694 |
. . . . . 6
|
139 | | ondomen 8860 |
. . . . . 6
|
140 | 125, 138,
139 | sylancr 695 |
. . . . 5
|
141 | | ffn 6045 |
. . . . . . 7
|
142 | 17, 141 | syl 17 |
. . . . . 6
|
143 | | dffn4 6121 |
. . . . . 6
|
144 | 142, 143 | sylib 208 |
. . . . 5
|
145 | | fodomnum 8880 |
. . . . 5
|
146 | 140, 144,
145 | sylc 65 |
. . . 4
|
147 | | domtr 8009 |
. . . 4
|
148 | 146, 138,
147 | syl2anc 693 |
. . 3
|
149 | | 2ndci 21251 |
. . 3
|
150 | 124, 148,
149 | syl2anc 693 |
. 2
|
151 | 121, 150 | eqeltrrd 2702 |
1
|