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 3772	. . . . . . . . 9 $/\$
2		xpnz 5244	. . . . . . . . . . 11 $/\$
3	2	biimpri 206	. . . . . . . . . 10 $/\$
4	3	simprd 461	. . . . . . . . 9
5	1, 4	syl 17	. . . . . . . 8 $/\$
6		dmxp 5042	. . . . . . . . . 10
7		dmss 5023	. . . . . . . . . . 11
8		sseq2 3464	. . . . . . . . . . 11
9	7, 8	syl5ib 219	. . . . . . . . . 10
10	6, 9	syl 17	. . . . . . . . 9
11	10	impcom 428	. . . . . . . 8 $/\$
12	5, 11	syldan 468	. . . . . . 7 $/\$
13		relxp 4931	. . . . . . . . . . 11
14		relss 4911	. . . . . . . . . . 11
15	13, 14	mpi 20	. . . . . . . . . 10
16		reldm0 5041	. . . . . . . . . 10
17	15, 16	syl 17	. . . . . . . . 9
18	17	necon3bid 2661	. . . . . . . 8
19	18	biimpa 482	. . . . . . 7 $/\$
20	12, 19	jca 530	. . . . . 6 $/\$ $/\$
21		df-fr 4782	. . . . . . 7 $/\$
22		vex 3062	. . . . . . . . 9
23	22	dmex 6717	. . . . . . . 8
24		sseq1 3463	. . . . . . . . . 10
25		neeq1 2684	. . . . . . . . . 10
26	24, 25	anbi12d 709	. . . . . . . . 9 $/\$ $/\$
27		raleq 3004	. . . . . . . . . 10
28	27	rexeqbi1dv 3013	. . . . . . . . 9
29	26, 28	imbi12d 318	. . . . . . . 8 $/\$ $/\$
30	23, 29	spcv 3150	. . . . . . 7 $/\$ $/\$
31	21, 30	sylbi 195	. . . . . 6 $/\$
32	20, 31	syl5 30	. . . . 5 $/\$
33	32	adantr 463	. . . 4 $/\$ $/\$
34		imassrn 5168	. . . . . . . . . . . . . . 15
35		xpeq0 5245	. . . . . . . . . . . . . . . . . . . 20 $\/$
36	35	biimpri 206	. . . . . . . . . . . . . . . . . . 19 $\/$
37	36	orcs 392	. . . . . . . . . . . . . . . . . 18
38		sseq2 3464	. . . . . . . . . . . . . . . . . . 19
39		ss0 3770	. . . . . . . . . . . . . . . . . . 19
40	38, 39	syl6bi 228	. . . . . . . . . . . . . . . . . 18
41	37, 40	syl 17	. . . . . . . . . . . . . . . . 17
42		rneq 5049	. . . . . . . . . . . . . . . . . 18
43		rn0 5075	. . . . . . . . . . . . . . . . . . 19
44		0ss 3768	. . . . . . . . . . . . . . . . . . 19
45	43, 44	eqsstri 3472	. . . . . . . . . . . . . . . . . 18
46	42, 45	syl6eqss 3492	. . . . . . . . . . . . . . . . 17
47	41, 46	syl6 31	. . . . . . . . . . . . . . . 16
48		rnxp 5255	. . . . . . . . . . . . . . . . 17
49		rnss 5052	. . . . . . . . . . . . . . . . . 18
50		sseq2 3464	. . . . . . . . . . . . . . . . . 18
51	49, 50	syl5ib 219	. . . . . . . . . . . . . . . . 17
52	48, 51	syl 17	. . . . . . . . . . . . . . . 16
53	47, 52	pm2.61ine 2716	. . . . . . . . . . . . . . 15
54	34, 53	syl5ss 3453	. . . . . . . . . . . . . 14
55		vex 3062	. . . . . . . . . . . . . . . 16
56	55	eldm 5021	. . . . . . . . . . . . . . 15
57		vex 3062	. . . . . . . . . . . . . . . . . . 19
58	55, 57	elimasn 5182	. . . . . . . . . . . . . . . . . 18
59		df-br 4396	. . . . . . . . . . . . . . . . . 18
60	58, 59	bitr4i 252	. . . . . . . . . . . . . . . . 17
61		ne0i 3744	. . . . . . . . . . . . . . . . 17
62	60, 61	sylbir 213	. . . . . . . . . . . . . . . 16
63	62	exlimiv 1743	. . . . . . . . . . . . . . 15
64	56, 63	sylbi 195	. . . . . . . . . . . . . 14
65		df-fr 4782	. . . . . . . . . . . . . . 15 $/\$
66		imaexg 6721	. . . . . . . . . . . . . . . . 17
67	22, 66	ax-mp 5	. . . . . . . . . . . . . . . 16
68		sseq1 3463	. . . . . . . . . . . . . . . . . 18
69		neeq1 2684	. . . . . . . . . . . . . . . . . 18
70	68, 69	anbi12d 709	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
71		raleq 3004	. . . . . . . . . . . . . . . . . 18
72	71	rexeqbi1dv 3013	. . . . . . . . . . . . . . . . 17
73	70, 72	imbi12d 318	. . . . . . . . . . . . . . . 16 $/\$ $/\$
74	67, 73	spcv 3150	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	65, 74	sylbi 195	. . . . . . . . . . . . . 14 $/\$
76	54, 64, 75	syl2ani 654	. . . . . . . . . . . . 13 $/\$
77		1stdm 6831	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
78		breq1 4398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
79	78	notbid 292	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
80	79	rspccv 3157	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
81	77, 80	syl5 30	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
82	81	expd 434	. . . . . . . . . . . . . . . . . . . . . . . . 25
83	82	impcom 428	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
84	83	adantr 463	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
85		elrel 4926	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
86	85	ex 432	. . . . . . . . . . . . . . . . . . . . . . . . . 26
87	86	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
88		vex 3062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
89	55, 88	elimasn 5182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
90		breq1 4398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
91	90	notbid 292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
92	91	rspccv 3157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
93	89, 92	syl5bir 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
94	93	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
95		opeq1 4159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
96	95	eleq1d 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
97	96	imbi1d 315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
98	94, 97	syl5ibr 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
99	98	com3l 81	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
100		eleq1 2474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101		vex 3062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
102	101, 88	op1std 6794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
103	102	eqeq1d 2404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
104	101, 88	op2ndd 6795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
105	104	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106	105	notbid 292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
107	103, 106	imbi12d 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
108	100, 107	imbi12d 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
109	99, 108	syl5ibr 221	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
110	109	exlimivv 1744	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
111	110	com3l 81	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
112	87, 111	mpdd 38	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
113	112	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
114	84, 113	jcad 531	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
115	114	ralrimiv 2816	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
116	115	ex 432	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
117	15, 116	sylan 469	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
118		olc 382	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\/$ $/\$
119	118	ralimi 2797	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\/$ $/\$
120	117, 119	syl6 31	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\/$ $/\$
121		ianor 486	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$
122		vex 3062	. . . . . . . . . . . . . . . . . . . . . 22
123		opex 4655	. . . . . . . . . . . . . . . . . . . . . 22
124		eleq1 2474	. . . . . . . . . . . . . . . . . . . . . . . 24
125	124	anbi1d 703	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
126		fveq2 5849	. . . . . . . . . . . . . . . . . . . . . . . . 25
127	126	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . 24
128	126	eqeq1d 2404	. . . . . . . . . . . . . . . . . . . . . . . . 25
129		fveq2 5849	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130	129	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	128, 130	anbi12d 709	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
132	127, 131	orbi12d 708	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $/\$ $\/$ $/\$
133	125, 132	anbi12d 709	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
134		eleq1 2474	. . . . . . . . . . . . . . . . . . . . . . . 24
135	134	anbi2d 702	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
136	55, 57	op1std 6794	. . . . . . . . . . . . . . . . . . . . . . . . 25
137	136	breq2d 4407	. . . . . . . . . . . . . . . . . . . . . . . 24
138	136	eqeq2d 2416	. . . . . . . . . . . . . . . . . . . . . . . . 25
139	55, 57	op2ndd 6795	. . . . . . . . . . . . . . . . . . . . . . . . . 26
140	139	breq2d 4407	. . . . . . . . . . . . . . . . . . . . . . . . 25
141	138, 140	anbi12d 709	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
142	137, 141	orbi12d 708	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $/\$ $\/$ $/\$
143	135, 142	anbi12d 709	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
144		frxp.1	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$
145	122, 123, 133, 143, 144	brab 4713	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\/$ $/\$
146	121, 145	xchnxbir 307	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\/$ $\/$ $/\$
147		ioran 488	. . . . . . . . . . . . . . . . . . . . . 22 $\/$ $/\$ $/\$ $/\$
148		ianor 486	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\/$
149		pm4.62 417	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
150	148, 149	bitr4i 252	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
151	150	anbi2i 692	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
152	147, 151	bitri 249	. . . . . . . . . . . . . . . . . . . . 21 $\/$ $/\$ $/\$
153	152	orbi2i 517	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$
154	146, 153	bitri 249	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$ $/\$
155	154	ralbii 2835	. . . . . . . . . . . . . . . . . 18 $/\$ $\/$ $/\$
156	120, 155	syl6ibr 227	. . . . . . . . . . . . . . . . 17 $/\$
157	156	reximdv 2878	. . . . . . . . . . . . . . . 16 $/\$
158	157	ex 432	. . . . . . . . . . . . . . 15
159	158	com23 78	. . . . . . . . . . . . . 14
160	159	adantr 463	. . . . . . . . . . . . 13 $/\$
161	76, 160	sylcom 27	. . . . . . . . . . . 12 $/\$
162	161	impl 618	. . . . . . . . . . 11 $/\$ $/\$
163	162	expimpd 601	. . . . . . . . . 10 $/\$ $/\$
164	163	3adant3 1017	. . . . . . . . 9 $/\$ $/\$ $/\$
165		resss 5117	. . . . . . . . . 10
166		df-rex 2760	. . . . . . . . . . . . 13 $/\$
167		eqid 2402	. . . . . . . . . . . . . . . 16
168		eqeq1 2406	. . . . . . . . . . . . . . . . . 18
169		breq2 4399	. . . . . . . . . . . . . . . . . . . . 21
170	169	notbid 292	. . . . . . . . . . . . . . . . . . . 20
171	170	ralbidv 2843	. . . . . . . . . . . . . . . . . . 19
172	171	anbi2d 702	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
173	168, 172	anbi12d 709	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
174	123, 173	spcev 3151	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
175	167, 174	mpan 668	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
176	58, 175	sylanb 470	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
177	176	eximi 1677	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
178	166, 177	sylbi 195	. . . . . . . . . . . 12 $/\$ $/\$
179		excom 1873	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
180	178, 179	sylib 196	. . . . . . . . . . 11 $/\$ $/\$
181		df-rex 2760	. . . . . . . . . . . 12 $/\$
182	55	elsnres 5130	. . . . . . . . . . . . . . 15 $/\$
183	182	anbi1i 693	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
184		19.41v 1795	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
185		anass 647	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
186	185	exbii 1688	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
187	183, 184, 186	3bitr2i 273	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
188	187	exbii 1688	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
189	181, 188	bitri 249	. . . . . . . . . . 11 $/\$ $/\$
190	180, 189	sylibr 212	. . . . . . . . . 10
191		ssrexv 3504	. . . . . . . . . 10
192	165, 190, 191	mpsyl 62	. . . . . . . . 9
193	164, 192	syl6 31	. . . . . . . 8 $/\$ $/\$ $/\$
194	193	expd 434	. . . . . . 7 $/\$ $/\$
195	194	rexlimdv 2894	. . . . . 6 $/\$ $/\$
196	195	3expib 1200	. . . . 5 $/\$
197	196	adantl 464	. . . 4 $/\$ $/\$
198	33, 197	mpdd 38	. . 3 $/\$ $/\$
199	198	alrimiv 1740	. 2 $/\$ $/\$
200		df-fr 4782	. 2 $/\$
201	199, 200	sylibr 212	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 366 $/\$ wa 367 $/\$ w3a 974

wal 1403

wceq 1405

wex 1633

wcel 1842

wne 2598

wral 2754

wrex 2755

cvv 3059

wss 3414

c0 3738

csn 3972

cop 3978 class class class wbr 4395

copab 4452

wfr 4779

cxp 4821

cdm 4823

crn 4824

cres 4825

cima 4826

wrel 4828

cfv 5569

c1st 6782

c2nd 6783

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-sep 4517 ax-nul 4525 ax-pow 4572 ax-pr 4630 ax-un 6574

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3an 976 df-tru 1408 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-ral 2759 df-rex 2760 df-rab 2763 df-v 3061 df-sbc 3278 df-dif 3417 df-un 3419 df-in 3421 df-ss 3428 df-nul 3739 df-if 3886 df-sn 3973 df-pr 3975 df-op 3979 df-uni 4192 df-int 4228 df-br 4396 df-opab 4454 df-mpt 4455 df-id 4738 df-fr 4782 df-xp 4829 df-rel 4830 df-cnv 4831 df-co 4832 df-dm 4833 df-rn 4834 df-res 4835 df-ima 4836 df-iota 5533 df-fun 5571 df-fv 5577 df-1st 6784 df-2nd 6785

This theorem is referenced by: wexp 6898

W3C validator