frxp - Metamath Proof Explorer

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

Theorem frxp 7287

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 3976	. . . . . . . . 9 $/\$
2		xpnz 5553	. . . . . . . . . . 11 $/\$
3	2	biimpri 218	. . . . . . . . . 10 $/\$
4	3	simprd 479	. . . . . . . . 9
5	1, 4	syl 17	. . . . . . . 8 $/\$
6		dmxp 5344	. . . . . . . . . 10
7		dmss 5323	. . . . . . . . . . 11
8		sseq2 3627	. . . . . . . . . . 11
9	7, 8	syl5ib 234	. . . . . . . . . 10
10	6, 9	syl 17	. . . . . . . . 9
11	10	impcom 446	. . . . . . . 8 $/\$
12	5, 11	syldan 487	. . . . . . 7 $/\$
13		relxp 5227	. . . . . . . . . . 11
14		relss 5206	. . . . . . . . . . 11
15	13, 14	mpi 20	. . . . . . . . . 10
16		reldm0 5343	. . . . . . . . . 10
17	15, 16	syl 17	. . . . . . . . 9
18	17	necon3bid 2838	. . . . . . . 8
19	18	biimpa 501	. . . . . . 7 $/\$
20	12, 19	jca 554	. . . . . 6 $/\$ $/\$
21		df-fr 5073	. . . . . . 7 $/\$
22		vex 3203	. . . . . . . . 9
23	22	dmex 7099	. . . . . . . 8
24		sseq1 3626	. . . . . . . . . 10
25		neeq1 2856	. . . . . . . . . 10
26	24, 25	anbi12d 747	. . . . . . . . 9 $/\$ $/\$
27		raleq 3138	. . . . . . . . . 10
28	27	rexeqbi1dv 3147	. . . . . . . . 9
29	26, 28	imbi12d 334	. . . . . . . 8 $/\$ $/\$
30	23, 29	spcv 3299	. . . . . . 7 $/\$ $/\$
31	21, 30	sylbi 207	. . . . . 6 $/\$
32	20, 31	syl5 34	. . . . 5 $/\$
33	32	adantr 481	. . . 4 $/\$ $/\$
34		imassrn 5477	. . . . . . . . . . . . . . 15
35		xpeq0 5554	. . . . . . . . . . . . . . . . . . . 20 $\/$
36	35	biimpri 218	. . . . . . . . . . . . . . . . . . 19 $\/$
37	36	orcs 409	. . . . . . . . . . . . . . . . . 18
38		sseq2 3627	. . . . . . . . . . . . . . . . . . 19
39		ss0 3974	. . . . . . . . . . . . . . . . . . 19
40	38, 39	syl6bi 243	. . . . . . . . . . . . . . . . . 18
41	37, 40	syl 17	. . . . . . . . . . . . . . . . 17
42		rneq 5351	. . . . . . . . . . . . . . . . . 18
43		rn0 5377	. . . . . . . . . . . . . . . . . . 19
44		0ss 3972	. . . . . . . . . . . . . . . . . . 19
45	43, 44	eqsstri 3635	. . . . . . . . . . . . . . . . . 18
46	42, 45	syl6eqss 3655	. . . . . . . . . . . . . . . . 17
47	41, 46	syl6 35	. . . . . . . . . . . . . . . 16
48		rnxp 5564	. . . . . . . . . . . . . . . . 17
49		rnss 5354	. . . . . . . . . . . . . . . . . 18
50		sseq2 3627	. . . . . . . . . . . . . . . . . 18
51	49, 50	syl5ib 234	. . . . . . . . . . . . . . . . 17
52	48, 51	syl 17	. . . . . . . . . . . . . . . 16
53	47, 52	pm2.61ine 2877	. . . . . . . . . . . . . . 15
54	34, 53	syl5ss 3614	. . . . . . . . . . . . . 14
55		vex 3203	. . . . . . . . . . . . . . . 16
56	55	eldm 5321	. . . . . . . . . . . . . . 15
57		vex 3203	. . . . . . . . . . . . . . . . . . 19
58	55, 57	elimasn 5490	. . . . . . . . . . . . . . . . . 18
59		df-br 4654	. . . . . . . . . . . . . . . . . 18
60	58, 59	bitr4i 267	. . . . . . . . . . . . . . . . 17
61		ne0i 3921	. . . . . . . . . . . . . . . . 17
62	60, 61	sylbir 225	. . . . . . . . . . . . . . . 16
63	62	exlimiv 1858	. . . . . . . . . . . . . . 15
64	56, 63	sylbi 207	. . . . . . . . . . . . . 14
65		df-fr 5073	. . . . . . . . . . . . . . 15 $/\$
66	22	imaex 7104	. . . . . . . . . . . . . . . 16
67		sseq1 3626	. . . . . . . . . . . . . . . . . 18
68		neeq1 2856	. . . . . . . . . . . . . . . . . 18
69	67, 68	anbi12d 747	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
70		raleq 3138	. . . . . . . . . . . . . . . . . 18
71	70	rexeqbi1dv 3147	. . . . . . . . . . . . . . . . 17
72	69, 71	imbi12d 334	. . . . . . . . . . . . . . . 16 $/\$ $/\$
73	66, 72	spcv 3299	. . . . . . . . . . . . . . 15 $/\$ $/\$
74	65, 73	sylbi 207	. . . . . . . . . . . . . 14 $/\$
75	54, 64, 74	syl2ani 688	. . . . . . . . . . . . 13 $/\$
76		1stdm 7215	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
77		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
78	77	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
79	78	rspccv 3306	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
80	76, 79	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
81	80	expd 452	. . . . . . . . . . . . . . . . . . . . . . . . 25
82	81	impcom 446	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
83	82	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
84		elrel 5222	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
85	84	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . 26
86	85	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
87		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
88	55, 87	elimasn 5490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
89		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
90	89	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
91	90	rspccv 3306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
92	88, 91	syl5bir 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
93	92	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
94		opeq1 4402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
95	94	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
96	95	imbi1d 331	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
97	93, 96	syl5ibr 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
98	97	com3l 89	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
99		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
100		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
101	100, 87	op1std 7178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
102	101	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
103	100, 87	op2ndd 7179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
104	103	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
105	104	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
106	102, 105	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
107	99, 106	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
108	98, 107	syl5ibr 236	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
109	108	exlimivv 1860	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
110	109	com3l 89	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
111	86, 110	mpdd 43	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
112	111	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
113	83, 112	jcad 555	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
114	113	ralrimiv 2965	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
115	114	ex 450	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
116	15, 115	sylan 488	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
117		olc 399	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\/$ $/\$
118	117	ralimi 2952	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\/$ $/\$
119	116, 118	syl6 35	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\/$ $/\$
120		ianor 509	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$
121		vex 3203	. . . . . . . . . . . . . . . . . . . . . 22
122		opex 4932	. . . . . . . . . . . . . . . . . . . . . 22
123		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . 24
124	123	anbi1d 741	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
125		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . 25
126	125	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . 24
127	125	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . 25
128		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . 26
129	128	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . . . 25
130	127, 129	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
131	126, 130	orbi12d 746	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $/\$ $\/$ $/\$
132	124, 131	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
133		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . 24
134	133	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
135	55, 57	op1std 7178	. . . . . . . . . . . . . . . . . . . . . . . . 25
136	135	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . 24
137	135	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . 25
138	55, 57	op2ndd 7179	. . . . . . . . . . . . . . . . . . . . . . . . . 26
139	138	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . 25
140	137, 139	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
141	136, 140	orbi12d 746	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $/\$ $\/$ $/\$
142	134, 141	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
143		frxp.1	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$
144	121, 122, 132, 142, 143	brab 4998	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\/$ $/\$
145	120, 144	xchnxbir 323	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\/$ $\/$ $/\$
146		ioran 511	. . . . . . . . . . . . . . . . . . . . . 22 $\/$ $/\$ $/\$ $/\$
147		ianor 509	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\/$
148		pm4.62 435	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
149	147, 148	bitr4i 267	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
150	149	anbi2i 730	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
151	146, 150	bitri 264	. . . . . . . . . . . . . . . . . . . . 21 $\/$ $/\$ $/\$
152	151	orbi2i 541	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$
153	145, 152	bitri 264	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$ $/\$
154	153	ralbii 2980	. . . . . . . . . . . . . . . . . 18 $/\$ $\/$ $/\$
155	119, 154	syl6ibr 242	. . . . . . . . . . . . . . . . 17 $/\$
156	155	reximdv 3016	. . . . . . . . . . . . . . . 16 $/\$
157	156	ex 450	. . . . . . . . . . . . . . 15
158	157	com23 86	. . . . . . . . . . . . . 14
159	158	adantr 481	. . . . . . . . . . . . 13 $/\$
160	75, 159	sylcom 30	. . . . . . . . . . . 12 $/\$
161	160	impl 650	. . . . . . . . . . 11 $/\$ $/\$
162	161	expimpd 629	. . . . . . . . . 10 $/\$ $/\$
163	162	3adant3 1081	. . . . . . . . 9 $/\$ $/\$ $/\$
164		resss 5422	. . . . . . . . . 10
165		df-rex 2918	. . . . . . . . . . . . 13 $/\$
166		eqid 2622	. . . . . . . . . . . . . . . 16
167		eqeq1 2626	. . . . . . . . . . . . . . . . . 18
168		breq2 4657	. . . . . . . . . . . . . . . . . . . . 21
169	168	notbid 308	. . . . . . . . . . . . . . . . . . . 20
170	169	ralbidv 2986	. . . . . . . . . . . . . . . . . . 19
171	170	anbi2d 740	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
172	167, 171	anbi12d 747	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
173	122, 172	spcev 3300	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
174	166, 173	mpan 706	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
175	58, 174	sylanb 489	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
176	175	eximi 1762	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
177	165, 176	sylbi 207	. . . . . . . . . . . 12 $/\$ $/\$
178		excom 2042	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
179	177, 178	sylib 208	. . . . . . . . . . 11 $/\$ $/\$
180		df-rex 2918	. . . . . . . . . . . 12 $/\$
181	55	elsnres 5436	. . . . . . . . . . . . . . 15 $/\$
182	181	anbi1i 731	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
183		19.41v 1914	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
184		anass 681	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
185	184	exbii 1774	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
186	182, 183, 185	3bitr2i 288	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
187	186	exbii 1774	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
188	180, 187	bitri 264	. . . . . . . . . . 11 $/\$ $/\$
189	179, 188	sylibr 224	. . . . . . . . . 10
190		ssrexv 3667	. . . . . . . . . 10
191	164, 189, 190	mpsyl 68	. . . . . . . . 9
192	163, 191	syl6 35	. . . . . . . 8 $/\$ $/\$ $/\$
193	192	expd 452	. . . . . . 7 $/\$ $/\$
194	193	rexlimdv 3030	. . . . . 6 $/\$ $/\$
195	194	3expib 1268	. . . . 5 $/\$
196	195	adantl 482	. . . 4 $/\$ $/\$
197	33, 196	mpdd 43	. . 3 $/\$ $/\$
198	197	alrimiv 1855	. 2 $/\$ $/\$
199		df-fr 5073	. 2 $/\$
200	198, 199	sylibr 224	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 $/\$ w3a 1037

wal 1481

wceq 1483

wex 1704

wcel 1990

wne 2794

wral 2912

wrex 2913

wss 3574

c0 3915

csn 4177

cop 4183 class class class wbr 4653

copab 4712

wfr 5070

cxp 5112

cdm 5114

crn 5115

cres 5116

cima 5117

wrel 5119

cfv 5888

c1st 7166

c2nd 7167

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-int 4476 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-fr 5073 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-iota 5851 df-fun 5890 df-fv 5896 df-1st 7168 df-2nd 7169

This theorem is referenced by: wexp 7291

W3C validator