frxp - Metamath Proof Explorer

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

Theorem frxp 6909

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:

Allowed substitution hints:

(

)

Proof of Theorem frxp Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssn0 3827	. . . . . . . . 9 $/\$
2		xpnz 5433	. . . . . . . . . . 11 $/\$
3	2	biimpri 206	. . . . . . . . . 10 $/\$
4	3	simprd 463	. . . . . . . . 9
5	1, 4	syl 16	. . . . . . . 8 $/\$
6		dmxp 5231	. . . . . . . . . 10
7		dmss 5212	. . . . . . . . . . 11
8		sseq2 3521	. . . . . . . . . . 11
9	7, 8	syl5ib 219	. . . . . . . . . 10
10	6, 9	syl 16	. . . . . . . . 9
11	10	impcom 430	. . . . . . . 8 $/\$
12	5, 11	syldan 470	. . . . . . 7 $/\$
13		relxp 5119	. . . . . . . . . . 11
14		relss 5099	. . . . . . . . . . 11
15	13, 14	mpi 17	. . . . . . . . . 10
16		reldm0 5230	. . . . . . . . . 10
17	15, 16	syl 16	. . . . . . . . 9
18	17	necon3bid 2715	. . . . . . . 8
19	18	biimpa 484	. . . . . . 7 $/\$
20	12, 19	jca 532	. . . . . 6 $/\$ $/\$
21		df-fr 4847	. . . . . . 7 $/\$
22		vex 3112	. . . . . . . . 9
23	22	dmex 6732	. . . . . . . 8
24		sseq1 3520	. . . . . . . . . 10
25		neeq1 2738	. . . . . . . . . 10
26	24, 25	anbi12d 710	. . . . . . . . 9 $/\$ $/\$
27		raleq 3054	. . . . . . . . . 10
28	27	rexeqbi1dv 3063	. . . . . . . . 9
29	26, 28	imbi12d 320	. . . . . . . 8 $/\$ $/\$
30	23, 29	spcv 3200	. . . . . . 7 $/\$ $/\$
31	21, 30	sylbi 195	. . . . . 6 $/\$
32	20, 31	syl5 32	. . . . 5 $/\$
33	32	adantr 465	. . . 4 $/\$ $/\$
34		imassrn 5358	. . . . . . . . . . . . . . 15
35		xpeq0 5434	. . . . . . . . . . . . . . . . . . . 20 $\/$
36	35	biimpri 206	. . . . . . . . . . . . . . . . . . 19 $\/$
37	36	orcs 394	. . . . . . . . . . . . . . . . . 18
38		sseq2 3521	. . . . . . . . . . . . . . . . . . 19
39		ss0 3825	. . . . . . . . . . . . . . . . . . 19
40	38, 39	syl6bi 228	. . . . . . . . . . . . . . . . . 18
41	37, 40	syl 16	. . . . . . . . . . . . . . . . 17
42		rneq 5238	. . . . . . . . . . . . . . . . . 18
43		rn0 5264	. . . . . . . . . . . . . . . . . . 19
44		0ss 3823	. . . . . . . . . . . . . . . . . . 19
45	43, 44	eqsstri 3529	. . . . . . . . . . . . . . . . . 18
46	42, 45	syl6eqss 3549	. . . . . . . . . . . . . . . . 17
47	41, 46	syl6 33	. . . . . . . . . . . . . . . 16
48		rnxp 5444	. . . . . . . . . . . . . . . . 17
49		rnss 5241	. . . . . . . . . . . . . . . . . 18
50		sseq2 3521	. . . . . . . . . . . . . . . . . 18
51	49, 50	syl5ib 219	. . . . . . . . . . . . . . . . 17
52	48, 51	syl 16	. . . . . . . . . . . . . . . 16
53	47, 52	pm2.61ine 2770	. . . . . . . . . . . . . . 15
54	34, 53	syl5ss 3510	. . . . . . . . . . . . . 14
55		vex 3112	. . . . . . . . . . . . . . . 16
56	55	eldm 5210	. . . . . . . . . . . . . . 15
57		vex 3112	. . . . . . . . . . . . . . . . . . 19
58	55, 57	elimasn 5372	. . . . . . . . . . . . . . . . . 18
59		df-br 4457	. . . . . . . . . . . . . . . . . 18
60	58, 59	bitr4i 252	. . . . . . . . . . . . . . . . 17
61		ne0i 3799	. . . . . . . . . . . . . . . . 17
62	60, 61	sylbir 213	. . . . . . . . . . . . . . . 16
63	62	exlimiv 1723	. . . . . . . . . . . . . . 15
64	56, 63	sylbi 195	. . . . . . . . . . . . . 14
65		df-fr 4847	. . . . . . . . . . . . . . 15 $/\$
66		imaexg 6736	. . . . . . . . . . . . . . . . 17
67	22, 66	ax-mp 5	. . . . . . . . . . . . . . . 16
68		sseq1 3520	. . . . . . . . . . . . . . . . . 18
69		neeq1 2738	. . . . . . . . . . . . . . . . . 18
70	68, 69	anbi12d 710	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
71		raleq 3054	. . . . . . . . . . . . . . . . . 18
72	71	rexeqbi1dv 3063	. . . . . . . . . . . . . . . . 17
73	70, 72	imbi12d 320	. . . . . . . . . . . . . . . 16 $/\$ $/\$
74	67, 73	spcv 3200	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	65, 74	sylbi 195	. . . . . . . . . . . . . 14 $/\$
76	54, 64, 75	syl2ani 656	. . . . . . . . . . . . 13 $/\$
77		1stdm 6846	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
78		breq1 4459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
79	78	notbid 294	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
80	79	rspccv 3207	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
81	77, 80	syl5 32	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
82	81	expd 436	. . . . . . . . . . . . . . . . . . . . . . . . 25
83	82	impcom 430	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
84	83	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
85		elrel 5114	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
86	85	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . 26
87	86	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
88		vex 3112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
89	55, 88	elimasn 5372	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
90		breq1 4459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
91	90	notbid 294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
92	91	rspccv 3207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
93	89, 92	syl5bir 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
94	93	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
95		opeq1 4219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
96	95	eleq1d 2526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
97	96	imbi1d 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
98	94, 97	syl5ibr 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
99	98	com3l 81	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
100		eleq1 2529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101		vex 3112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
102	101, 88	op1std 6809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
103	102	eqeq1d 2459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
104	101, 88	op2ndd 6810	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
105	104	breq1d 4466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106	105	notbid 294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
107	103, 106	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
108	100, 107	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
109	99, 108	syl5ibr 221	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
110	109	exlimivv 1724	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
111	110	com3l 81	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
112	87, 111	mpdd 40	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
113	112	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
114	84, 113	jcad 533	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
115	114	ralrimiv 2869	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
116	115	ex 434	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
117	15, 116	sylan 471	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
118		olc 384	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\/$ $/\$
119	118	ralimi 2850	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\/$ $/\$
120	117, 119	syl6 33	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\/$ $/\$
121		ianor 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$
122		vex 3112	. . . . . . . . . . . . . . . . . . . . . 22
123		opex 4720	. . . . . . . . . . . . . . . . . . . . . 22
124		eleq1 2529	. . . . . . . . . . . . . . . . . . . . . . . 24
125	124	anbi1d 704	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
126		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . 25
127	126	breq1d 4466	. . . . . . . . . . . . . . . . . . . . . . . 24
128	126	eqeq1d 2459	. . . . . . . . . . . . . . . . . . . . . . . . 25
129		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130	129	breq1d 4466	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	128, 130	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
132	127, 131	orbi12d 709	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $/\$ $\/$ $/\$
133	125, 132	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
134		eleq1 2529	. . . . . . . . . . . . . . . . . . . . . . . 24
135	134	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
136	55, 57	op1std 6809	. . . . . . . . . . . . . . . . . . . . . . . . 25
137	136	breq2d 4468	. . . . . . . . . . . . . . . . . . . . . . . 24
138	136	eqeq2d 2471	. . . . . . . . . . . . . . . . . . . . . . . . 25
139	55, 57	op2ndd 6810	. . . . . . . . . . . . . . . . . . . . . . . . . 26
140	139	breq2d 4468	. . . . . . . . . . . . . . . . . . . . . . . . 25
141	138, 140	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
142	137, 141	orbi12d 709	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $/\$ $\/$ $/\$
143	135, 142	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
144		frxp.1	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$
145	122, 123, 133, 143, 144	brab 4779	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\/$ $/\$
146	121, 145	xchnxbir 309	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\/$ $\/$ $/\$
147		ioran 490	. . . . . . . . . . . . . . . . . . . . . 22 $\/$ $/\$ $/\$ $/\$
148		ianor 488	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\/$
149		pm4.62 419	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
150	148, 149	bitr4i 252	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
151	150	anbi2i 694	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
152	147, 151	bitri 249	. . . . . . . . . . . . . . . . . . . . 21 $\/$ $/\$ $/\$
153	152	orbi2i 519	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$
154	146, 153	bitri 249	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$ $/\$
155	154	ralbii 2888	. . . . . . . . . . . . . . . . . 18 $/\$ $\/$ $/\$
156	120, 155	syl6ibr 227	. . . . . . . . . . . . . . . . 17 $/\$
157	156	reximdv 2931	. . . . . . . . . . . . . . . 16 $/\$
158	157	ex 434	. . . . . . . . . . . . . . 15
159	158	com23 78	. . . . . . . . . . . . . 14
160	159	adantr 465	. . . . . . . . . . . . 13 $/\$
161	76, 160	sylcom 29	. . . . . . . . . . . 12 $/\$
162	161	impl 620	. . . . . . . . . . 11 $/\$ $/\$
163	162	expimpd 603	. . . . . . . . . 10 $/\$ $/\$
164	163	3adant3 1016	. . . . . . . . 9 $/\$ $/\$ $/\$
165		resss 5307	. . . . . . . . . 10
166		df-rex 2813	. . . . . . . . . . . . 13 $/\$
167		eqid 2457	. . . . . . . . . . . . . . . 16
168		eqeq1 2461	. . . . . . . . . . . . . . . . . 18
169		breq2 4460	. . . . . . . . . . . . . . . . . . . . 21
170	169	notbid 294	. . . . . . . . . . . . . . . . . . . 20
171	170	ralbidv 2896	. . . . . . . . . . . . . . . . . . 19
172	171	anbi2d 703	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
173	168, 172	anbi12d 710	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
174	123, 173	spcev 3201	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
175	167, 174	mpan 670	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
176	58, 175	sylanb 472	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
177	176	eximi 1657	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
178	166, 177	sylbi 195	. . . . . . . . . . . 12 $/\$ $/\$
179		excom 1850	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
180	178, 179	sylib 196	. . . . . . . . . . 11 $/\$ $/\$
181		df-rex 2813	. . . . . . . . . . . 12 $/\$
182	55	elsnres 5320	. . . . . . . . . . . . . . 15 $/\$
183	182	anbi1i 695	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
184		19.41v 1772	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
185		anass 649	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
186	185	exbii 1668	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
187	183, 184, 186	3bitr2i 273	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
188	187	exbii 1668	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
189	181, 188	bitri 249	. . . . . . . . . . 11 $/\$ $/\$
190	180, 189	sylibr 212	. . . . . . . . . 10
191		ssrexv 3561	. . . . . . . . . 10
192	165, 190, 191	mpsyl 63	. . . . . . . . 9
193	164, 192	syl6 33	. . . . . . . 8 $/\$ $/\$ $/\$
194	193	expd 436	. . . . . . 7 $/\$ $/\$
195	194	rexlimdv 2947	. . . . . 6 $/\$ $/\$
196	195	3expib 1199	. . . . 5 $/\$
197	196	adantl 466	. . . 4 $/\$ $/\$
198	33, 197	mpdd 40	. . 3 $/\$ $/\$
199	198	alrimiv 1720	. 2 $/\$ $/\$
200		df-fr 4847	. 2 $/\$
201	199, 200	sylibr 212	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $/\$ w3a 973

wal 1393

wceq 1395

wex 1613

wcel 1819

wne 2652

wral 2807

wrex 2808

cvv 3109

wss 3471

c0 3793

csn 4032

cop 4038 class class class wbr 4456

copab 4514

wfr 4844

cxp 5006

cdm 5008

crn 5009

cres 5010

cima 5011

wrel 5013

cfv 5594

c1st 6797

c2nd 6798

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-ral 2812 df-rex 2813 df-rab 2816 df-v 3111 df-sbc 3328 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-nul 3794 df-if 3945 df-sn 4033 df-pr 4035 df-op 4039 df-uni 4252 df-int 4289 df-br 4457 df-opab 4516 df-mpt 4517 df-id 4804 df-fr 4847 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fv 5602 df-1st 6799 df-2nd 6800

This theorem is referenced by: wexp 6913

W3C validator