MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frxp Unicode version

Theorem frxp 6910
Description: A lexicographical ordering of two well-founded classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) (Proof shortened by Wolf Lammen, 4-Oct-2014.)
Hypothesis
Ref Expression
frxp.1
Assertion
Ref Expression
frxp
Distinct variable groups:   , ,   , ,   , ,   ,S,

Proof of Theorem frxp
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssn0 3818 . . . . . . . . 9
2 xpnz 5431 . . . . . . . . . . 11
32biimpri 206 . . . . . . . . . 10
43simprd 463 . . . . . . . . 9
51, 4syl 16 . . . . . . . 8
6 dmxp 5226 . . . . . . . . . 10
7 dmss 5207 . . . . . . . . . . 11
8 sseq2 3525 . . . . . . . . . . 11
97, 8syl5ib 219 . . . . . . . . . 10
106, 9syl 16 . . . . . . . . 9
1110impcom 430 . . . . . . . 8
125, 11syldan 470 . . . . . . 7
13 relxp 5115 . . . . . . . . . . 11
14 relss 5095 . . . . . . . . . . 11
1513, 14mpi 17 . . . . . . . . . 10
16 reldm0 5225 . . . . . . . . . 10
1715, 16syl 16 . . . . . . . . 9
1817necon3bid 2715 . . . . . . . 8
1918biimpa 484 . . . . . . 7
2012, 19jca 532 . . . . . 6
21 df-fr 4843 . . . . . . 7
22 vex 3112 . . . . . . . . 9
2322dmex 6733 . . . . . . . 8
24 sseq1 3524 . . . . . . . . . 10
25 neeq1 2738 . . . . . . . . . 10
2624, 25anbi12d 710 . . . . . . . . 9
27 raleq 3054 . . . . . . . . . 10
2827rexeqbi1dv 3063 . . . . . . . . 9
2926, 28imbi12d 320 . . . . . . . 8
3023, 29spcv 3200 . . . . . . 7
3121, 30sylbi 195 . . . . . 6
3220, 31syl5 32 . . . . 5
3332adantr 465 . . . 4
34 imassrn 5353 . . . . . . . . . . . . . . 15
35 xpeq0 5432 . . . . . . . . . . . . . . . . . . . 20
3635biimpri 206 . . . . . . . . . . . . . . . . . . 19
3736orcs 394 . . . . . . . . . . . . . . . . . 18
38 sseq2 3525 . . . . . . . . . . . . . . . . . . 19
39 ss0 3816 . . . . . . . . . . . . . . . . . . 19
4038, 39syl6bi 228 . . . . . . . . . . . . . . . . . 18
4137, 40syl 16 . . . . . . . . . . . . . . . . 17
42 rneq 5233 . . . . . . . . . . . . . . . . . 18
43 rn0 5259 . . . . . . . . . . . . . . . . . . 19
44 0ss 3814 . . . . . . . . . . . . . . . . . . 19
4543, 44eqsstri 3533 . . . . . . . . . . . . . . . . . 18
4642, 45syl6eqss 3553 . . . . . . . . . . . . . . . . 17
4741, 46syl6 33 . . . . . . . . . . . . . . . 16
48 rnxp 5442 . . . . . . . . . . . . . . . . 17
49 rnss 5236 . . . . . . . . . . . . . . . . . 18
50 sseq2 3525 . . . . . . . . . . . . . . . . . 18
5149, 50syl5ib 219 . . . . . . . . . . . . . . . . 17
5248, 51syl 16 . . . . . . . . . . . . . . . 16
5347, 52pm2.61ine 2770 . . . . . . . . . . . . . . 15
5434, 53syl5ss 3514 . . . . . . . . . . . . . 14
55 vex 3112 . . . . . . . . . . . . . . . 16
5655eldm 5205 . . . . . . . . . . . . . . 15
57 vex 3112 . . . . . . . . . . . . . . . . . . 19
5855, 57elimasn 5367 . . . . . . . . . . . . . . . . . 18
59 df-br 4453 . . . . . . . . . . . . . . . . . 18
6058, 59bitr4i 252 . . . . . . . . . . . . . . . . 17
61 ne0i 3790 . . . . . . . . . . . . . . . . 17
6260, 61sylbir 213 . . . . . . . . . . . . . . . 16
6362exlimiv 1722 . . . . . . . . . . . . . . 15
6456, 63sylbi 195 . . . . . . . . . . . . . 14
65 df-fr 4843 . . . . . . . . . . . . . . 15
66 imaexg 6737 . . . . . . . . . . . . . . . . 17
6722, 66ax-mp 5 . . . . . . . . . . . . . . . 16
68 sseq1 3524 . . . . . . . . . . . . . . . . . 18
69 neeq1 2738 . . . . . . . . . . . . . . . . . 18
7068, 69anbi12d 710 . . . . . . . . . . . . . . . . 17
71 raleq 3054 . . . . . . . . . . . . . . . . . 18
7271rexeqbi1dv 3063 . . . . . . . . . . . . . . . . 17
7370, 72imbi12d 320 . . . . . . . . . . . . . . . 16
7467, 73spcv 3200 . . . . . . . . . . . . . . 15
7565, 74sylbi 195 . . . . . . . . . . . . . 14
7654, 64, 75syl2ani 656 . . . . . . . . . . . . 13
77 1stdm 6847 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
78 breq1 4455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7978notbid 294 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8079rspccv 3207 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8177, 80syl5 32 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8281expd 436 . . . . . . . . . . . . . . . . . . . . . . . . 25
8382impcom 430 . . . . . . . . . . . . . . . . . . . . . . . 24
8483adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23
85 elrel 5110 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8685ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8786adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
88 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
8955, 88elimasn 5367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
90 breq1 4455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
9190notbid 294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
9291rspccv 3207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
9389, 92syl5bir 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
9493adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
95 opeq1 4217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
9695eleq1d 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
9796imbi1d 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
9894, 97syl5ibr 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9998com3l 81 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
100 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
102101, 88op1std 6810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
103102eqeq1d 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
104101, 88op2ndd 6811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
105104breq1d 4462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106105notbid 294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
107103, 106imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
108100, 107imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
10999, 108syl5ibr 221 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
110109exlimivv 1723 . . . . . . . . . . . . . . . . . . . . . . . . . 26
111110com3l 81 . . . . . . . . . . . . . . . . . . . . . . . . 25
11287, 111mpdd 40 . . . . . . . . . . . . . . . . . . . . . . . 24
113112adantlr 714 . . . . . . . . . . . . . . . . . . . . . . 23
11484, 113jcad 533 . . . . . . . . . . . . . . . . . . . . . 22
115114ralrimiv 2869 . . . . . . . . . . . . . . . . . . . . 21
116115ex 434 . . . . . . . . . . . . . . . . . . . 20
11715, 116sylan 471 . . . . . . . . . . . . . . . . . . 19
118 olc 384 . . . . . . . . . . . . . . . . . . . 20
119118ralimi 2850 . . . . . . . . . . . . . . . . . . 19
120117, 119syl6 33 . . . . . . . . . . . . . . . . . 18
121 ianor 488 . . . . . . . . . . . . . . . . . . . . 21
122 vex 3112 . . . . . . . . . . . . . . . . . . . . . 22
123 opex 4716 . . . . . . . . . . . . . . . . . . . . . 22
124 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . . . 24
125124anbi1d 704 . . . . . . . . . . . . . . . . . . . . . . 23
126 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . 25
127126breq1d 4462 . . . . . . . . . . . . . . . . . . . . . . . 24
128126eqeq1d 2459 . . . . . . . . . . . . . . . . . . . . . . . . 25
129 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . 26
130129breq1d 4462 . . . . . . . . . . . . . . . . . . . . . . . . 25
131128, 130anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . 24
132127, 131orbi12d 709 . . . . . . . . . . . . . . . . . . . . . . 23
133125, 132anbi12d 710 . . . . . . . . . . . . . . . . . . . . . 22
134 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . . . 24
135134anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . 23
13655, 57op1std 6810 . . . . . . . . . . . . . . . . . . . . . . . . 25
137136breq2d 4464 . . . . . . . . . . . . . . . . . . . . . . . 24
138136eqeq2d 2471 . . . . . . . . . . . . . . . . . . . . . . . . 25
13955, 57op2ndd 6811 . . . . . . . . . . . . . . . . . . . . . . . . . 26
140139breq2d 4464 . . . . . . . . . . . . . . . . . . . . . . . . 25
141138, 140anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . 24
142137, 141orbi12d 709 . . . . . . . . . . . . . . . . . . . . . . 23
143135, 142anbi12d 710 . . . . . . . . . . . . . . . . . . . . . 22
144 frxp.1 . . . . . . . . . . . . . . . . . . . . . 22
145122, 123, 133, 143, 144brab 4775 . . . . . . . . . . . . . . . . . . . . 21
146121, 145xchnxbir 309 . . . . . . . . . . . . . . . . . . . 20
147 ioran 490 . . . . . . . . . . . . . . . . . . . . . 22
148 ianor 488 . . . . . . . . . . . . . . . . . . . . . . . 24
149 pm4.62 419 . . . . . . . . . . . . . . . . . . . . . . . 24
150148, 149bitr4i 252 . . . . . . . . . . . . . . . . . . . . . . 23
151150anbi2i 694 . . . . . . . . . . . . . . . . . . . . . 22
152147, 151bitri 249 . . . . . . . . . . . . . . . . . . . . 21
153152orbi2i 519 . . . . . . . . . . . . . . . . . . . 20
154146, 153bitri 249 . . . . . . . . . . . . . . . . . . 19
155154ralbii 2888 . . . . . . . . . . . . . . . . . 18
156120, 155syl6ibr 227 . . . . . . . . . . . . . . . . 17
157156reximdv 2931 . . . . . . . . . . . . . . . 16
158157ex 434 . . . . . . . . . . . . . . 15
159158com23 78 . . . . . . . . . . . . . 14
160159adantr 465 . . . . . . . . . . . . 13
16176, 160sylcom 29 . . . . . . . . . . . 12
162161impl 620 . . . . . . . . . . 11
163162expimpd 603 . . . . . . . . . 10
1641633adant3 1016 . . . . . . . . 9
165 resss 5302 . . . . . . . . . 10
166 df-rex 2813 . . . . . . . . . . . . 13
167 eqid 2457 . . . . . . . . . . . . . . . 16
168 eqeq1 2461 . . . . . . . . . . . . . . . . . 18
169 breq2 4456 . . . . . . . . . . . . . . . . . . . . 21
170169notbid 294 . . . . . . . . . . . . . . . . . . . 20
171170ralbidv 2896 . . . . . . . . . . . . . . . . . . 19
172171anbi2d 703 . . . . . . . . . . . . . . . . . 18
173168, 172anbi12d 710 . . . . . . . . . . . . . . . . 17
174123, 173spcev 3201 . . . . . . . . . . . . . . . 16
175167, 174mpan 670 . . . . . . . . . . . . . . 15
17658, 175sylanb 472 . . . . . . . . . . . . . 14
177176eximi 1656 . . . . . . . . . . . . 13
178166, 177sylbi 195 . . . . . . . . . . . 12
179 excom 1849 . . . . . . . . . . . 12
180178, 179sylib 196 . . . . . . . . . . 11
181 df-rex 2813 . . . . . . . . . . . 12
18255elsnres 5315 . . . . . . . . . . . . . . 15
183182anbi1i 695 . . . . . . . . . . . . . 14
184 19.41v 1771 . . . . . . . . . . . . . 14
185 anass 649 . . . . . . . . . . . . . . 15