frxp - Metamath Proof Explorer

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

Theorem frxp 6894

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 3818	. . . . . . . . 9 $/\$
2		xpnz 5426	. . . . . . . . . . 11 $/\$
3	2	biimpri 206	. . . . . . . . . 10 $/\$
4	3	simprd 463	. . . . . . . . 9
5	1, 4	syl 16	. . . . . . . 8 $/\$
6		dmxp 5221	. . . . . . . . . 10
7		dmss 5202	. . . . . . . . . . 11
8		sseq2 3526	. . . . . . . . . . 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 5110	. . . . . . . . . . 11
14		relss 5090	. . . . . . . . . . 11
15	13, 14	mpi 17	. . . . . . . . . 10
16		reldm0 5220	. . . . . . . . . 10
17	15, 16	syl 16	. . . . . . . . 9
18	17	necon3bid 2725	. . . . . . . 8
19	18	biimpa 484	. . . . . . 7 $/\$
20	12, 19	jca 532	. . . . . 6 $/\$ $/\$
21		df-fr 4838	. . . . . . 7 $/\$
22		vex 3116	. . . . . . . . 9
23	22	dmex 6718	. . . . . . . 8
24		sseq1 3525	. . . . . . . . . 10
25		neeq1 2748	. . . . . . . . . 10
26	24, 25	anbi12d 710	. . . . . . . . 9 $/\$ $/\$
27		raleq 3058	. . . . . . . . . 10
28	27	rexeqbi1dv 3067	. . . . . . . . 9
29	26, 28	imbi12d 320	. . . . . . . 8 $/\$ $/\$
30	23, 29	spcv 3204	. . . . . . 7 $/\$ $/\$
31	21, 30	sylbi 195	. . . . . 6 $/\$
32	20, 31	syl5 32	. . . . 5 $/\$
33	32	adantr 465	. . . 4 $/\$ $/\$
34		imassrn 5348	. . . . . . . . . . . . . . 15
35		xpeq0 5427	. . . . . . . . . . . . . . . . . . . 20 $\/$
36	35	biimpri 206	. . . . . . . . . . . . . . . . . . 19 $\/$
37	36	orcs 394	. . . . . . . . . . . . . . . . . 18
38		sseq2 3526	. . . . . . . . . . . . . . . . . . 19
39		ss0 3816	. . . . . . . . . . . . . . . . . . 19
40	38, 39	syl6bi 228	. . . . . . . . . . . . . . . . . 18
41	37, 40	syl 16	. . . . . . . . . . . . . . . . 17
42		rneq 5228	. . . . . . . . . . . . . . . . . 18
43		rn0 5254	. . . . . . . . . . . . . . . . . . 19
44		0ss 3814	. . . . . . . . . . . . . . . . . . 19
45	43, 44	eqsstri 3534	. . . . . . . . . . . . . . . . . 18
46	42, 45	syl6eqss 3554	. . . . . . . . . . . . . . . . 17
47	41, 46	syl6 33	. . . . . . . . . . . . . . . 16
48		rnxp 5437	. . . . . . . . . . . . . . . . 17
49		rnss 5231	. . . . . . . . . . . . . . . . . 18
50		sseq2 3526	. . . . . . . . . . . . . . . . . 18
51	49, 50	syl5ib 219	. . . . . . . . . . . . . . . . 17
52	48, 51	syl 16	. . . . . . . . . . . . . . . 16
53	47, 52	pm2.61ine 2780	. . . . . . . . . . . . . . 15
54	34, 53	syl5ss 3515	. . . . . . . . . . . . . 14
55		vex 3116	. . . . . . . . . . . . . . . 16
56	55	eldm 5200	. . . . . . . . . . . . . . 15
57		vex 3116	. . . . . . . . . . . . . . . . . . 19
58	55, 57	elimasn 5362	. . . . . . . . . . . . . . . . . 18
59		df-br 4448	. . . . . . . . . . . . . . . . . 18
60	58, 59	bitr4i 252	. . . . . . . . . . . . . . . . 17
61		ne0i 3791	. . . . . . . . . . . . . . . . 17
62	60, 61	sylbir 213	. . . . . . . . . . . . . . . 16
63	62	exlimiv 1698	. . . . . . . . . . . . . . 15
64	56, 63	sylbi 195	. . . . . . . . . . . . . 14
65		df-fr 4838	. . . . . . . . . . . . . . 15 $/\$
66		imaexg 6722	. . . . . . . . . . . . . . . . 17
67	22, 66	ax-mp 5	. . . . . . . . . . . . . . . 16
68		sseq1 3525	. . . . . . . . . . . . . . . . . 18
69		neeq1 2748	. . . . . . . . . . . . . . . . . 18
70	68, 69	anbi12d 710	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
71		raleq 3058	. . . . . . . . . . . . . . . . . 18
72	71	rexeqbi1dv 3067	. . . . . . . . . . . . . . . . 17
73	70, 72	imbi12d 320	. . . . . . . . . . . . . . . 16 $/\$ $/\$
74	67, 73	spcv 3204	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	65, 74	sylbi 195	. . . . . . . . . . . . . 14 $/\$
76	54, 64, 75	syl2ani 656	. . . . . . . . . . . . 13 $/\$
77		1stdm 6832	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
78		breq1 4450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
79	78	notbid 294	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
80	79	rspccv 3211	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
81	77, 80	syl5 32	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
82	81	expd 436	. . . . . . . . . . . . . . . . . . . . . . . . 25
83	82	impcom 430	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
84	83	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
85		elrel 5105	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
86	85	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . 26
87	86	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
88		vex 3116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
89	55, 88	elimasn 5362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
90		breq1 4450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
91	90	notbid 294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
92	91	rspccv 3211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
93	89, 92	syl5bir 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
94	93	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
95		opeq1 4213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
96	95	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
97	96	imbi1d 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
98	94, 97	syl5ibr 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
99	98	com3l 81	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
100		eleq1 2539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101		vex 3116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
102	101, 88	op1std 6795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
103	102	eqeq1d 2469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
104	101, 88	op2ndd 6796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
105	104	breq1d 4457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1699	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2876	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
116	115	ex 434	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
117	15, 116	sylan 471	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
118		olc 384	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\/$ $/\$
119	118	ralimi 2857	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\/$ $/\$
120	117, 119	syl6 33	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\/$ $/\$
121		ianor 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$
122		vex 3116	. . . . . . . . . . . . . . . . . . . . . 22
123		opex 4711	. . . . . . . . . . . . . . . . . . . . . 22
124		eleq1 2539	. . . . . . . . . . . . . . . . . . . . . . . 24
125	124	anbi1d 704	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
126		fveq2 5866	. . . . . . . . . . . . . . . . . . . . . . . . 25
127	126	breq1d 4457	. . . . . . . . . . . . . . . . . . . . . . . 24
128	126	eqeq1d 2469	. . . . . . . . . . . . . . . . . . . . . . . . 25
129		fveq2 5866	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130	129	breq1d 4457	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	128, 130	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
132	127, 131	orbi12d 709	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $/\$ $\/$ $/\$
133	125, 132	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
134		eleq1 2539	. . . . . . . . . . . . . . . . . . . . . . . 24
135	134	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
136	55, 57	op1std 6795	. . . . . . . . . . . . . . . . . . . . . . . . 25
137	136	breq2d 4459	. . . . . . . . . . . . . . . . . . . . . . . 24
138	136	eqeq2d 2481	. . . . . . . . . . . . . . . . . . . . . . . . 25
139	55, 57	op2ndd 6796	. . . . . . . . . . . . . . . . . . . . . . . . . 26
140	139	breq2d 4459	. . . . . . . . . . . . . . . . . . . . . . . . 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 4770	. . . . . . . . . . . . . . . . . . . . 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 2895	. . . . . . . . . . . . . . . . . 18 $/\$ $\/$ $/\$
156	120, 155	syl6ibr 227	. . . . . . . . . . . . . . . . 17 $/\$
157	156	reximdv 2937	. . . . . . . . . . . . . . . 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 5297	. . . . . . . . . 10
166		df-rex 2820	. . . . . . . . . . . . 13 $/\$
167		eqid 2467	. . . . . . . . . . . . . . . 16
168		eqeq1 2471	. . . . . . . . . . . . . . . . . 18
169		breq2 4451	. . . . . . . . . . . . . . . . . . . . 21
170	169	notbid 294	. . . . . . . . . . . . . . . . . . . 20
171	170	ralbidv 2903	. . . . . . . . . . . . . . . . . . 19
172	171	anbi2d 703	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
173	168, 172	anbi12d 710	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
174	123, 173	spcev 3205	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
175	167, 174	mpan 670	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
176	58, 175	sylanb 472	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
177	176	eximi 1635	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
178	166, 177	sylbi 195	. . . . . . . . . . . 12 $/\$ $/\$
179		excom 1798	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
180	178, 179	sylib 196	. . . . . . . . . . 11 $/\$ $/\$
181		df-rex 2820	. . . . . . . . . . . 12 $/\$
182	55	elsnres 5310	. . . . . . . . . . . . . . 15 $/\$
183	182	anbi1i 695	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
184		19.41v 1945	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
185		anass 649	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
186	185	exbii 1644	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
187	183, 184, 186	3bitr2i 273	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
188	187	exbii 1644	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
189	181, 188	bitri 249	. . . . . . . . . . 11 $/\$ $/\$
190	180, 189	sylibr 212	. . . . . . . . . 10
191		ssrexv 3565	. . . . . . . . . 10
192	165, 190, 191	mpsyl 63	. . . . . . . . 9
193	164, 192	syl6 33	. . . . . . . 8 $/\$ $/\$ $/\$
194	193	expd 436	. . . . . . 7 $/\$ $/\$
195	194	rexlimdv 2953	. . . . . 6 $/\$ $/\$
196	195	3expib 1199	. . . . 5 $/\$
197	196	adantl 466	. . . 4 $/\$ $/\$
198	33, 197	mpdd 40	. . 3 $/\$ $/\$
199	198	alrimiv 1695	. 2 $/\$ $/\$
200		df-fr 4838	. 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 1377

wceq 1379

wex 1596

wcel 1767

wne 2662

wral 2814

wrex 2815

cvv 3113

wss 3476

c0 3785

csn 4027

cop 4033 class class class wbr 4447

copab 4504

wfr 4835

cxp 4997

cdm 4999

crn 5000

cres 5001

cima 5002

wrel 5004

cfv 5588

c1st 6783

c2nd 6784

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6577

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-ral 2819 df-rex 2820 df-rab 2823 df-v 3115 df-sbc 3332 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-nul 3786 df-if 3940 df-sn 4028 df-pr 4030 df-op 4034 df-uni 4246 df-int 4283 df-br 4448 df-opab 4506 df-mpt 4507 df-id 4795 df-fr 4838 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fv 5596 df-1st 6785 df-2nd 6786

This theorem is referenced by: wexp 6898

W3C validator