frxp - Metamath Proof Explorer

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

Theorem frxp 6703

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 3691	. . . . . . . . 9 $/\$
2		xpnz 5278	. . . . . . . . . . 11 $/\$
3	2	biimpri 206	. . . . . . . . . 10 $/\$
4	3	simprd 463	. . . . . . . . 9
5	1, 4	syl 16	. . . . . . . 8 $/\$
6		dmxp 5079	. . . . . . . . . 10
7		dmss 5060	. . . . . . . . . . 11
8		sseq2 3399	. . . . . . . . . . 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 4968	. . . . . . . . . . 11
14		relss 4948	. . . . . . . . . . 11
15	13, 14	mpi 17	. . . . . . . . . 10
16		reldm0 5078	. . . . . . . . . 10
17	15, 16	syl 16	. . . . . . . . 9
18	17	necon3bid 2637	. . . . . . . 8
19	18	biimpa 484	. . . . . . 7 $/\$
20	12, 19	jca 532	. . . . . 6 $/\$ $/\$
21		df-fr 4700	. . . . . . 7 $/\$
22		vex 2996	. . . . . . . . 9
23	22	dmex 6532	. . . . . . . 8
24		sseq1 3398	. . . . . . . . . 10
25		neeq1 2644	. . . . . . . . . 10
26	24, 25	anbi12d 710	. . . . . . . . 9 $/\$ $/\$
27		raleq 2938	. . . . . . . . . 10
28	27	rexeqbi1dv 2947	. . . . . . . . 9
29	26, 28	imbi12d 320	. . . . . . . 8 $/\$ $/\$
30	23, 29	spcv 3084	. . . . . . 7 $/\$ $/\$
31	21, 30	sylbi 195	. . . . . 6 $/\$
32	20, 31	syl5 32	. . . . 5 $/\$
33	32	adantr 465	. . . 4 $/\$ $/\$
34		imassrn 5201	. . . . . . . . . . . . . . 15
35		xpeq0 5279	. . . . . . . . . . . . . . . . . . . 20 $\/$
36	35	biimpri 206	. . . . . . . . . . . . . . . . . . 19 $\/$
37	36	orcs 394	. . . . . . . . . . . . . . . . . 18
38		sseq2 3399	. . . . . . . . . . . . . . . . . . 19
39		ss0 3689	. . . . . . . . . . . . . . . . . . 19
40	38, 39	syl6bi 228	. . . . . . . . . . . . . . . . . 18
41	37, 40	syl 16	. . . . . . . . . . . . . . . . 17
42		rneq 5086	. . . . . . . . . . . . . . . . . 18
43		rn0 5112	. . . . . . . . . . . . . . . . . . 19
44		0ss 3687	. . . . . . . . . . . . . . . . . . 19
45	43, 44	eqsstri 3407	. . . . . . . . . . . . . . . . . 18
46	42, 45	syl6eqss 3427	. . . . . . . . . . . . . . . . 17
47	41, 46	syl6 33	. . . . . . . . . . . . . . . 16
48		rnxp 5289	. . . . . . . . . . . . . . . . 17
49		rnss 5089	. . . . . . . . . . . . . . . . . 18
50		sseq2 3399	. . . . . . . . . . . . . . . . . 18
51	49, 50	syl5ib 219	. . . . . . . . . . . . . . . . 17
52	48, 51	syl 16	. . . . . . . . . . . . . . . 16
53	47, 52	pm2.61ine 2711	. . . . . . . . . . . . . . 15
54	34, 53	syl5ss 3388	. . . . . . . . . . . . . 14
55		vex 2996	. . . . . . . . . . . . . . . 16
56	55	eldm 5058	. . . . . . . . . . . . . . 15
57		vex 2996	. . . . . . . . . . . . . . . . . . 19
58	55, 57	elimasn 5215	. . . . . . . . . . . . . . . . . 18
59		df-br 4314	. . . . . . . . . . . . . . . . . 18
60	58, 59	bitr4i 252	. . . . . . . . . . . . . . . . 17
61		ne0i 3664	. . . . . . . . . . . . . . . . 17
62	60, 61	sylbir 213	. . . . . . . . . . . . . . . 16
63	62	exlimiv 1688	. . . . . . . . . . . . . . 15
64	56, 63	sylbi 195	. . . . . . . . . . . . . 14
65		df-fr 4700	. . . . . . . . . . . . . . 15 $/\$
66		imaexg 6536	. . . . . . . . . . . . . . . . 17
67	22, 66	ax-mp 5	. . . . . . . . . . . . . . . 16
68		sseq1 3398	. . . . . . . . . . . . . . . . . 18
69		neeq1 2644	. . . . . . . . . . . . . . . . . 18
70	68, 69	anbi12d 710	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
71		raleq 2938	. . . . . . . . . . . . . . . . . 18
72	71	rexeqbi1dv 2947	. . . . . . . . . . . . . . . . 17
73	70, 72	imbi12d 320	. . . . . . . . . . . . . . . 16 $/\$ $/\$
74	67, 73	spcv 3084	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	65, 74	sylbi 195	. . . . . . . . . . . . . 14 $/\$
76	54, 64, 75	syl2ani 656	. . . . . . . . . . . . 13 $/\$
77		1stdm 6642	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
78		breq1 4316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
79	78	notbid 294	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
80	79	rspccv 3091	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
81	77, 80	syl5 32	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
82	81	expd 436	. . . . . . . . . . . . . . . . . . . . . . . . 25
83	82	impcom 430	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
84	83	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
85		elrel 4963	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
86	85	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . 26
87	86	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
88		vex 2996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
89	55, 88	elimasn 5215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
90		breq1 4316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
91	90	notbid 294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
92	91	rspccv 3091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
93	89, 92	syl5bir 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
94	93	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
95		opeq1 4080	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
96	95	eleq1d 2509	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
97	96	imbi1d 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
98	94, 97	syl5ibr 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
99	98	com3l 81	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
100		eleq1 2503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101		vex 2996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
102	101, 88	op1std 6608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
103	102	eqeq1d 2451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
104	101, 88	op2ndd 6609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
105	104	breq1d 4323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1689	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2819	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
116	115	ex 434	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
117	15, 116	sylan 471	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
118		olc 384	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\/$ $/\$
119	118	ralimi 2812	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\/$ $/\$
120	117, 119	syl6 33	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\/$ $/\$
121		ianor 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$
122		vex 2996	. . . . . . . . . . . . . . . . . . . . . 22
123		opex 4577	. . . . . . . . . . . . . . . . . . . . . 22
124		eleq1 2503	. . . . . . . . . . . . . . . . . . . . . . . 24
125	124	anbi1d 704	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
126		fveq2 5712	. . . . . . . . . . . . . . . . . . . . . . . . 25
127	126	breq1d 4323	. . . . . . . . . . . . . . . . . . . . . . . 24
128	126	eqeq1d 2451	. . . . . . . . . . . . . . . . . . . . . . . . 25
129		fveq2 5712	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130	129	breq1d 4323	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	128, 130	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
132	127, 131	orbi12d 709	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $/\$ $\/$ $/\$
133	125, 132	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
134		eleq1 2503	. . . . . . . . . . . . . . . . . . . . . . . 24
135	134	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
136	55, 57	op1std 6608	. . . . . . . . . . . . . . . . . . . . . . . . 25
137	136	breq2d 4325	. . . . . . . . . . . . . . . . . . . . . . . 24
138	136	eqeq2d 2454	. . . . . . . . . . . . . . . . . . . . . . . . 25
139	55, 57	op2ndd 6609	. . . . . . . . . . . . . . . . . . . . . . . . . 26
140	139	breq2d 4325	. . . . . . . . . . . . . . . . . . . . . . . . 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 4632	. . . . . . . . . . . . . . . . . . . . 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 2760	. . . . . . . . . . . . . . . . . 18 $/\$ $\/$ $/\$
156	120, 155	syl6ibr 227	. . . . . . . . . . . . . . . . 17 $/\$
157	156	reximdv 2848	. . . . . . . . . . . . . . . 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 1008	. . . . . . . . 9 $/\$ $/\$ $/\$
165		resss 5155	. . . . . . . . . 10
166		df-rex 2742	. . . . . . . . . . . . 13 $/\$
167		eqid 2443	. . . . . . . . . . . . . . . 16
168		eqeq1 2449	. . . . . . . . . . . . . . . . . 18
169		breq2 4317	. . . . . . . . . . . . . . . . . . . . 21
170	169	notbid 294	. . . . . . . . . . . . . . . . . . . 20
171	170	ralbidv 2756	. . . . . . . . . . . . . . . . . . 19
172	171	anbi2d 703	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
173	168, 172	anbi12d 710	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
174	123, 173	spcev 3085	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
175	167, 174	mpan 670	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
176	58, 175	sylanb 472	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
177	176	eximi 1625	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
178	166, 177	sylbi 195	. . . . . . . . . . . 12 $/\$ $/\$
179		excom 1787	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
180	178, 179	sylib 196	. . . . . . . . . . 11 $/\$ $/\$
181		df-rex 2742	. . . . . . . . . . . 12 $/\$
182	55	elsnres 5167	. . . . . . . . . . . . . . 15 $/\$
183	182	anbi1i 695	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
184		19.41v 1920	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
185		anass 649	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
186	185	exbii 1634	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
187	183, 184, 186	3bitr2i 273	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
188	187	exbii 1634	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
189	181, 188	bitri 249	. . . . . . . . . . 11 $/\$ $/\$
190	180, 189	sylibr 212	. . . . . . . . . 10
191		ssrexv 3438	. . . . . . . . . 10
192	165, 190, 191	mpsyl 63	. . . . . . . . 9
193	164, 192	syl6 33	. . . . . . . 8 $/\$ $/\$ $/\$
194	193	expd 436	. . . . . . 7 $/\$ $/\$
195	194	rexlimdv 2861	. . . . . 6 $/\$ $/\$
196	195	3expib 1190	. . . . 5 $/\$
197	196	adantl 466	. . . 4 $/\$ $/\$
198	33, 197	mpdd 40	. . 3 $/\$ $/\$
199	198	alrimiv 1685	. 2 $/\$ $/\$
200		df-fr 4700	. 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 965

wal 1367

wceq 1369

wex 1586

wcel 1756

wne 2620

wral 2736

wrex 2737

cvv 2993

wss 3349

c0 3658

csn 3898

cop 3904 class class class wbr 4313

copab 4370

wfr 4697

cxp 4859

cdm 4861

crn 4862

cres 4863

cima 4864

wrel 4866

cfv 5439

c1st 6596

c2nd 6597

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-sep 4434 ax-nul 4442 ax-pow 4491 ax-pr 4552 ax-un 6393

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2577 df-ne 2622 df-ral 2741 df-rex 2742 df-rab 2745 df-v 2995 df-sbc 3208 df-dif 3352 df-un 3354 df-in 3356 df-ss 3363 df-nul 3659 df-if 3813 df-sn 3899 df-pr 3901 df-op 3905 df-uni 4113 df-int 4150 df-br 4314 df-opab 4372 df-mpt 4373 df-id 4657 df-fr 4700 df-xp 4867 df-rel 4868 df-cnv 4869 df-co 4870 df-dm 4871 df-rn 4872 df-res 4873 df-ima 4874 df-iota 5402 df-fun 5441 df-fv 5447 df-1st 6598 df-2nd 6599

This theorem is referenced by: wexp 6707

W3C validator