Step | Hyp | Ref
| Expression |
1 | | elex 3212 |
. 2
|
2 | | nosupno.1 |
. . 3
|
3 | | iftrue 4092 |
. . . . . 6
|
4 | 3 | adantr 481 |
. . . . 5
|
5 | | simprl 794 |
. . . . . . 7
|
6 | | simpl 473 |
. . . . . . . . 9
|
7 | | nomaxmo 31847 |
. . . . . . . . . 10
|
8 | 7 | ad2antrl 764 |
. . . . . . . . 9
|
9 | | reu5 3159 |
. . . . . . . . 9
|
10 | 6, 8, 9 | sylanbrc 698 |
. . . . . . . 8
|
11 | | riotacl 6625 |
. . . . . . . 8
|
12 | 10, 11 | syl 17 |
. . . . . . 7
|
13 | 5, 12 | sseldd 3604 |
. . . . . 6
|
14 | | 2on 7568 |
. . . . . . . . 9
|
15 | 14 | elexi 3213 |
. . . . . . . 8
|
16 | 15 | prid2 4298 |
. . . . . . 7
|
17 | 16 | noextend 31819 |
. . . . . 6
|
18 | 13, 17 | syl 17 |
. . . . 5
|
19 | 4, 18 | eqeltrd 2701 |
. . . 4
|
20 | | iffalse 4095 |
. . . . . 6
|
21 | 20 | adantr 481 |
. . . . 5
|
22 | | funmpt 5926 |
. . . . . . 7
|
23 | 22 | a1i 11 |
. . . . . 6
|
24 | | iotaex 5868 |
. . . . . . . . 9
|
25 | | eqid 2622 |
. . . . . . . . 9
|
26 | 24, 25 | dmmpti 6023 |
. . . . . . . 8
|
27 | | ssel2 3598 |
. . . . . . . . . . . . . . . . 17
|
28 | | nodmon 31803 |
. . . . . . . . . . . . . . . . 17
|
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . 16
|
30 | | onss 6990 |
. . . . . . . . . . . . . . . 16
|
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . . 15
|
32 | 31 | sseld 3602 |
. . . . . . . . . . . . . 14
|
33 | 32 | adantrd 484 |
. . . . . . . . . . . . 13
|
34 | 33 | rexlimdva 3031 |
. . . . . . . . . . . 12
|
35 | 34 | abssdv 3676 |
. . . . . . . . . . 11
|
36 | | simplr 792 |
. . . . . . . . . . . . . . . . . . 19
|
37 | 29 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . 20
|
38 | | ontr1 5771 |
. . . . . . . . . . . . . . . . . . . 20
|
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
40 | 36, 39 | mpand 711 |
. . . . . . . . . . . . . . . . . 18
|
41 | 40 | adantrd 484 |
. . . . . . . . . . . . . . . . 17
|
42 | | reseq1 5390 |
. . . . . . . . . . . . . . . . . . . . 21
|
43 | | onelon 5748 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
44 | 37, 43 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
45 | | suceloni 7013 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
47 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
48 | | eloni 5733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
49 | 44, 48 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
50 | | ordsucelsuc 7022 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
52 | 47, 51 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
53 | | onelss 5766 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
54 | 46, 52, 53 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
55 | 54 | resabs1d 5428 |
. . . . . . . . . . . . . . . . . . . . . 22
|
56 | 54 | resabs1d 5428 |
. . . . . . . . . . . . . . . . . . . . . 22
|
57 | 55, 56 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . . . . . 21
|
58 | 42, 57 | syl5ib 234 |
. . . . . . . . . . . . . . . . . . . 20
|
59 | 58 | imim2d 57 |
. . . . . . . . . . . . . . . . . . 19
|
60 | 59 | ralimdv 2963 |
. . . . . . . . . . . . . . . . . 18
|
61 | 60 | expimpd 629 |
. . . . . . . . . . . . . . . . 17
|
62 | 41, 61 | jcad 555 |
. . . . . . . . . . . . . . . 16
|
63 | 62 | reximdva 3017 |
. . . . . . . . . . . . . . 15
|
64 | 63 | expimpd 629 |
. . . . . . . . . . . . . 14
|
65 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
66 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . 18
|
67 | | suceq 5790 |
. . . . . . . . . . . . . . . . . . . . . 22
|
68 | 67 | reseq2d 5396 |
. . . . . . . . . . . . . . . . . . . . 21
|
69 | 67 | reseq2d 5396 |
. . . . . . . . . . . . . . . . . . . . 21
|
70 | 68, 69 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . . . . 20
|
71 | 70 | imbi2d 330 |
. . . . . . . . . . . . . . . . . . 19
|
72 | 71 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . 18
|
73 | 66, 72 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
|
74 | 73 | rexbidv 3052 |
. . . . . . . . . . . . . . . 16
|
75 | 65, 74 | elab 3350 |
. . . . . . . . . . . . . . 15
|
76 | 75 | anbi2i 730 |
. . . . . . . . . . . . . 14
|
77 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
78 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
|
79 | | suceq 5790 |
. . . . . . . . . . . . . . . . . . . . 21
|
80 | 79 | reseq2d 5396 |
. . . . . . . . . . . . . . . . . . . 20
|
81 | 79 | reseq2d 5396 |
. . . . . . . . . . . . . . . . . . . 20
|
82 | 80, 81 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . . . 19
|
83 | 82 | imbi2d 330 |
. . . . . . . . . . . . . . . . . 18
|
84 | 83 | ralbidv 2986 |
. . . . . . . . . . . . . . . . 17
|
85 | 78, 84 | anbi12d 747 |
. . . . . . . . . . . . . . . 16
|
86 | 85 | rexbidv 3052 |
. . . . . . . . . . . . . . 15
|
87 | 77, 86 | elab 3350 |
. . . . . . . . . . . . . 14
|
88 | 64, 76, 87 | 3imtr4g 285 |
. . . . . . . . . . . . 13
|
89 | 88 | alrimivv 1856 |
. . . . . . . . . . . 12
|
90 | | dftr2 4754 |
. . . . . . . . . . . 12
|
91 | 89, 90 | sylibr 224 |
. . . . . . . . . . 11
|
92 | | dford5 31608 |
. . . . . . . . . . 11
|
93 | 35, 91, 92 | sylanbrc 698 |
. . . . . . . . . 10
|
94 | 93 | adantr 481 |
. . . . . . . . 9
|
95 | | bdayfo 31828 |
. . . . . . . . . . . . . . 15
|
96 | | fofun 6116 |
. . . . . . . . . . . . . . 15
|
97 | 95, 96 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
98 | | funimaexg 5975 |
. . . . . . . . . . . . . 14
|
99 | 97, 98 | mpan 706 |
. . . . . . . . . . . . 13
|
100 | | uniexg 6955 |
. . . . . . . . . . . . 13
|
101 | 99, 100 | syl 17 |
. . . . . . . . . . . 12
|
102 | 101 | adantl 482 |
. . . . . . . . . . 11
|
103 | | simpl 473 |
. . . . . . . . . . . . . 14
|
104 | 103 | reximi 3011 |
. . . . . . . . . . . . 13
|
105 | 104 | ss2abi 3674 |
. . . . . . . . . . . 12
|
106 | | bdayval 31801 |
. . . . . . . . . . . . . . . . . . 19
|
107 | 27, 106 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
108 | | fofn 6117 |
. . . . . . . . . . . . . . . . . . . 20
|
109 | 95, 108 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
110 | | fnfvima 6496 |
. . . . . . . . . . . . . . . . . . 19
|
111 | 109, 110 | mp3an1 1411 |
. . . . . . . . . . . . . . . . . 18
|
112 | 107, 111 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . 17
|
113 | | elssuni 4467 |
. . . . . . . . . . . . . . . . 17
|
114 | 112, 113 | syl 17 |
. . . . . . . . . . . . . . . 16
|
115 | 114 | sseld 3602 |
. . . . . . . . . . . . . . 15
|
116 | 115 | rexlimdva 3031 |
. . . . . . . . . . . . . 14
|
117 | 116 | abssdv 3676 |
. . . . . . . . . . . . 13
|
118 | 117 | adantr 481 |
. . . . . . . . . . . 12
|
119 | 105, 118 | syl5ss 3614 |
. . . . . . . . . . 11
|
120 | 102, 119 | ssexd 4805 |
. . . . . . . . . 10
|
121 | | elong 5731 |
. . . . . . . . . 10
|
122 | 120, 121 | syl 17 |
. . . . . . . . 9
|
123 | 94, 122 | mpbird 247 |
. . . . . . . 8
|
124 | 26, 123 | syl5eqel 2705 |
. . . . . . 7
|
125 | 124 | adantl 482 |
. . . . . 6
|
126 | 25 | rnmpt 5371 |
. . . . . . . 8
|
127 | | vex 3203 |
. . . . . . . . . . . 12
|
128 | | eleq1 2689 |
. . . . . . . . . . . . . 14
|
129 | | suceq 5790 |
. . . . . . . . . . . . . . . . . 18
|
130 | 129 | reseq2d 5396 |
. . . . . . . . . . . . . . . . 17
|
131 | 129 | reseq2d 5396 |
. . . . . . . . . . . . . . . . 17
|
132 | 130, 131 | eqeq12d 2637 |
. . . . . . . . . . . . . . . 16
|
133 | 132 | imbi2d 330 |
. . . . . . . . . . . . . . 15
|
134 | 133 | ralbidv 2986 |
. . . . . . . . . . . . . 14
|
135 | 128, 134 | anbi12d 747 |
. . . . . . . . . . . . 13
|
136 | 135 | rexbidv 3052 |
. . . . . . . . . . . 12
|
137 | 127, 136 | elab 3350 |
. . . . . . . . . . 11
|
138 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
|
139 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . 20
|
140 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . . . . . 21
|
141 | 140 | 3anbi3d 1405 |
. . . . . . . . . . . . . . . . . . . 20
|
142 | 139, 141 | spcev 3300 |
. . . . . . . . . . . . . . . . . . 19
|
143 | 138, 142 | mp3an3 1413 |
. . . . . . . . . . . . . . . . . 18
|
144 | 143 | reximi 3011 |
. . . . . . . . . . . . . . . . 17
|
145 | | rexcom4 3225 |
. . . . . . . . . . . . . . . . 17
|
146 | 144, 145 | sylib 208 |
. . . . . . . . . . . . . . . 16
|
147 | 146 | adantl 482 |
. . . . . . . . . . . . . . 15
|
148 | | noprefixmo 31848 |
. . . . . . . . . . . . . . . 16
|
149 | 148 | adantr 481 |
. . . . . . . . . . . . . . 15
|
150 | | eu5 2496 |
. . . . . . . . . . . . . . 15
|
151 | 147, 149,
150 | sylanbrc 698 |
. . . . . . . . . . . . . 14
|
152 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
153 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . . 18
|
154 | 153 | 3anbi3d 1405 |
. . . . . . . . . . . . . . . . 17
|
155 | 154 | rexbidv 3052 |
. . . . . . . . . . . . . . . 16
|
156 | 155 | iota2 5877 |
. . . . . . . . . . . . . . 15
|
157 | 152, 156 | mpan 706 |
. . . . . . . . . . . . . 14
|
158 | 151, 157 | syl 17 |
. . . . . . . . . . . . 13
|
159 | | eqcom 2629 |
. . . . . . . . . . . . 13
|
160 | 158, 159 | syl6bb 276 |
. . . . . . . . . . . 12
|
161 | | simprr3 1111 |
. . . . . . . . . . . . . . 15
|
162 | 27 | adantrr 753 |
. . . . . . . . . . . . . . . . 17
|
163 | | norn 31804 |
. . . . . . . . . . . . . . . . 17
|
164 | 162, 163 | syl 17 |
. . . . . . . . . . . . . . . 16
|
165 | | nofun 31802 |
. . . . . . . . . . . . . . . . . 18
|
166 | 162, 165 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
167 | | simprr1 1109 |
. . . . . . . . . . . . . . . . 17
|
168 | | fvelrn 6352 |
. . . . . . . . . . . . . . . . 17
|
169 | 166, 167,
168 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
170 | 164, 169 | sseldd 3604 |
. . . . . . . . . . . . . . 15
|
171 | 161, 170 | eqeltrrd 2702 |
. . . . . . . . . . . . . 14
|
172 | 171 | rexlimdvaa 3032 |
. . . . . . . . . . . . 13
|
173 | 172 | adantr 481 |
. . . . . . . . . . . 12
|
174 | 160, 173 | sylbird 250 |
. . . . . . . . . . 11
|
175 | 137, 174 | sylan2b 492 |
. . . . . . . . . 10
|
176 | 175 | rexlimdva 3031 |
. . . . . . . . 9
|
177 | 176 | abssdv 3676 |
. . . . . . . 8
|
178 | 126, 177 | syl5eqss 3649 |
. . . . . . 7
|
179 | 178 | ad2antrl 764 |
. . . . . 6
|
180 | | elno2 31807 |
. . . . . 6
|
181 | 23, 125, 179, 180 | syl3anbrc 1246 |
. . . . 5
|
182 | 21, 181 | eqeltrd 2701 |
. . . 4
|
183 | 19, 182 | pm2.61ian 831 |
. . 3
|
184 | 2, 183 | syl5eqel 2705 |
. 2
|
185 | 1, 184 | sylan2 491 |
1
|