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 6925

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 3770	. . . . . . . . 9 $/\$
2		xpnz 5262	. . . . . . . . . . 11 $/\$
3	2	biimpri 211	. . . . . . . . . 10 $/\$
4	3	simprd 470	. . . . . . . . 9
5	1, 4	syl 17	. . . . . . . 8 $/\$
6		dmxp 5059	. . . . . . . . . 10
7		dmss 5039	. . . . . . . . . . 11
8		sseq2 3440	. . . . . . . . . . 11
9	7, 8	syl5ib 227	. . . . . . . . . 10
10	6, 9	syl 17	. . . . . . . . 9
11	10	impcom 437	. . . . . . . 8 $/\$
12	5, 11	syldan 478	. . . . . . 7 $/\$
13		relxp 4947	. . . . . . . . . . 11
14		relss 4927	. . . . . . . . . . 11
15	13, 14	mpi 20	. . . . . . . . . 10
16		reldm0 5058	. . . . . . . . . 10
17	15, 16	syl 17	. . . . . . . . 9
18	17	necon3bid 2687	. . . . . . . 8
19	18	biimpa 492	. . . . . . 7 $/\$
20	12, 19	jca 541	. . . . . 6 $/\$ $/\$
21		df-fr 4798	. . . . . . 7 $/\$
22		vex 3034	. . . . . . . . 9
23	22	dmex 6745	. . . . . . . 8
24		sseq1 3439	. . . . . . . . . 10
25		neeq1 2705	. . . . . . . . . 10
26	24, 25	anbi12d 725	. . . . . . . . 9 $/\$ $/\$
27		raleq 2973	. . . . . . . . . 10
28	27	rexeqbi1dv 2982	. . . . . . . . 9
29	26, 28	imbi12d 327	. . . . . . . 8 $/\$ $/\$
30	23, 29	spcv 3126	. . . . . . 7 $/\$ $/\$
31	21, 30	sylbi 200	. . . . . 6 $/\$
32	20, 31	syl5 32	. . . . 5 $/\$
33	32	adantr 472	. . . 4 $/\$ $/\$
34		imassrn 5185	. . . . . . . . . . . . . . 15
35		xpeq0 5263	. . . . . . . . . . . . . . . . . . . 20 $\/$
36	35	biimpri 211	. . . . . . . . . . . . . . . . . . 19 $\/$
37	36	orcs 401	. . . . . . . . . . . . . . . . . 18
38		sseq2 3440	. . . . . . . . . . . . . . . . . . 19
39		ss0 3768	. . . . . . . . . . . . . . . . . . 19
40	38, 39	syl6bi 236	. . . . . . . . . . . . . . . . . 18
41	37, 40	syl 17	. . . . . . . . . . . . . . . . 17
42		rneq 5066	. . . . . . . . . . . . . . . . . 18
43		rn0 5092	. . . . . . . . . . . . . . . . . . 19
44		0ss 3766	. . . . . . . . . . . . . . . . . . 19
45	43, 44	eqsstri 3448	. . . . . . . . . . . . . . . . . 18
46	42, 45	syl6eqss 3468	. . . . . . . . . . . . . . . . 17
47	41, 46	syl6 33	. . . . . . . . . . . . . . . 16
48		rnxp 5273	. . . . . . . . . . . . . . . . 17
49		rnss 5069	. . . . . . . . . . . . . . . . . 18
50		sseq2 3440	. . . . . . . . . . . . . . . . . 18
51	49, 50	syl5ib 227	. . . . . . . . . . . . . . . . 17
52	48, 51	syl 17	. . . . . . . . . . . . . . . 16
53	47, 52	pm2.61ine 2726	. . . . . . . . . . . . . . 15
54	34, 53	syl5ss 3429	. . . . . . . . . . . . . 14
55		vex 3034	. . . . . . . . . . . . . . . 16
56	55	eldm 5037	. . . . . . . . . . . . . . 15
57		vex 3034	. . . . . . . . . . . . . . . . . . 19
58	55, 57	elimasn 5199	. . . . . . . . . . . . . . . . . 18
59		df-br 4396	. . . . . . . . . . . . . . . . . 18
60	58, 59	bitr4i 260	. . . . . . . . . . . . . . . . 17
61		ne0i 3728	. . . . . . . . . . . . . . . . 17
62	60, 61	sylbir 218	. . . . . . . . . . . . . . . 16
63	62	exlimiv 1784	. . . . . . . . . . . . . . 15
64	56, 63	sylbi 200	. . . . . . . . . . . . . 14
65		df-fr 4798	. . . . . . . . . . . . . . 15 $/\$
66		imaexg 6749	. . . . . . . . . . . . . . . . 17
67	22, 66	ax-mp 5	. . . . . . . . . . . . . . . 16
68		sseq1 3439	. . . . . . . . . . . . . . . . . 18
69		neeq1 2705	. . . . . . . . . . . . . . . . . 18
70	68, 69	anbi12d 725	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
71		raleq 2973	. . . . . . . . . . . . . . . . . 18
72	71	rexeqbi1dv 2982	. . . . . . . . . . . . . . . . 17
73	70, 72	imbi12d 327	. . . . . . . . . . . . . . . 16 $/\$ $/\$
74	67, 73	spcv 3126	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	65, 74	sylbi 200	. . . . . . . . . . . . . 14 $/\$
76	54, 64, 75	syl2ani 668	. . . . . . . . . . . . 13 $/\$
77		1stdm 6859	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
78		breq1 4398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
79	78	notbid 301	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
80	79	rspccv 3133	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
81	77, 80	syl5 32	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
82	81	expd 443	. . . . . . . . . . . . . . . . . . . . . . . . 25
83	82	impcom 437	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
84	83	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
85		elrel 4942	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
86	85	ex 441	. . . . . . . . . . . . . . . . . . . . . . . . . 26
87	86	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
88		vex 3034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
89	55, 88	elimasn 5199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
90		breq1 4398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
91	90	notbid 301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
92	91	rspccv 3133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
93	89, 92	syl5bir 226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
94	93	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
95		opeq1 4158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
96	95	eleq1d 2533	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
97	96	imbi1d 324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
98	94, 97	syl5ibr 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
99	98	com3l 83	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
100		eleq1 2537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101		vex 3034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
102	101, 88	op1std 6822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
103	102	eqeq1d 2473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
104	101, 88	op2ndd 6823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
105	104	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106	105	notbid 301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
107	103, 106	imbi12d 327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
108	100, 107	imbi12d 327	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
109	99, 108	syl5ibr 229	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
110	109	exlimivv 1786	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
111	110	com3l 83	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
112	87, 111	mpdd 40	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
113	112	adantlr 729	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
114	84, 113	jcad 542	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
115	114	ralrimiv 2808	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
116	115	ex 441	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
117	15, 116	sylan 479	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
118		olc 391	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\/$ $/\$
119	118	ralimi 2796	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\/$ $/\$
120	117, 119	syl6 33	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\/$ $/\$
121		ianor 496	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$
122		vex 3034	. . . . . . . . . . . . . . . . . . . . . 22
123		opex 4664	. . . . . . . . . . . . . . . . . . . . . 22
124		eleq1 2537	. . . . . . . . . . . . . . . . . . . . . . . 24
125	124	anbi1d 719	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
126		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . 25
127	126	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . 24
128	126	eqeq1d 2473	. . . . . . . . . . . . . . . . . . . . . . . . 25
129		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130	129	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	128, 130	anbi12d 725	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
132	127, 131	orbi12d 724	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $/\$ $\/$ $/\$
133	125, 132	anbi12d 725	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
134		eleq1 2537	. . . . . . . . . . . . . . . . . . . . . . . 24
135	134	anbi2d 718	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
136	55, 57	op1std 6822	. . . . . . . . . . . . . . . . . . . . . . . . 25
137	136	breq2d 4407	. . . . . . . . . . . . . . . . . . . . . . . 24
138	136	eqeq2d 2481	. . . . . . . . . . . . . . . . . . . . . . . . 25
139	55, 57	op2ndd 6823	. . . . . . . . . . . . . . . . . . . . . . . . . 26
140	139	breq2d 4407	. . . . . . . . . . . . . . . . . . . . . . . . 25
141	138, 140	anbi12d 725	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
142	137, 141	orbi12d 724	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $/\$ $\/$ $/\$
143	135, 142	anbi12d 725	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
144		frxp.1	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$
145	122, 123, 133, 143, 144	brab 4724	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\/$ $/\$
146	121, 145	xchnxbir 316	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\/$ $\/$ $/\$
147		ioran 498	. . . . . . . . . . . . . . . . . . . . . 22 $\/$ $/\$ $/\$ $/\$
148		ianor 496	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\/$
149		pm4.62 426	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
150	148, 149	bitr4i 260	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
151	150	anbi2i 708	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
152	147, 151	bitri 257	. . . . . . . . . . . . . . . . . . . . 21 $\/$ $/\$ $/\$
153	152	orbi2i 528	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$
154	146, 153	bitri 257	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$ $/\$
155	154	ralbii 2823	. . . . . . . . . . . . . . . . . 18 $/\$ $\/$ $/\$
156	120, 155	syl6ibr 235	. . . . . . . . . . . . . . . . 17 $/\$
157	156	reximdv 2857	. . . . . . . . . . . . . . . 16 $/\$
158	157	ex 441	. . . . . . . . . . . . . . 15
159	158	com23 80	. . . . . . . . . . . . . 14
160	159	adantr 472	. . . . . . . . . . . . 13 $/\$
161	76, 160	sylcom 29	. . . . . . . . . . . 12 $/\$
162	161	impl 632	. . . . . . . . . . 11 $/\$ $/\$
163	162	expimpd 614	. . . . . . . . . 10 $/\$ $/\$
164	163	3adant3 1050	. . . . . . . . 9 $/\$ $/\$ $/\$
165		resss 5134	. . . . . . . . . 10
166		df-rex 2762	. . . . . . . . . . . . 13 $/\$
167		eqid 2471	. . . . . . . . . . . . . . . 16
168		eqeq1 2475	. . . . . . . . . . . . . . . . . 18
169		breq2 4399	. . . . . . . . . . . . . . . . . . . . 21
170	169	notbid 301	. . . . . . . . . . . . . . . . . . . 20
171	170	ralbidv 2829	. . . . . . . . . . . . . . . . . . 19
172	171	anbi2d 718	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
173	168, 172	anbi12d 725	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
174	123, 173	spcev 3127	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
175	167, 174	mpan 684	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
176	58, 175	sylanb 480	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
177	176	eximi 1715	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
178	166, 177	sylbi 200	. . . . . . . . . . . 12 $/\$ $/\$
179		excom 1944	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
180	178, 179	sylib 201	. . . . . . . . . . 11 $/\$ $/\$
181		df-rex 2762	. . . . . . . . . . . 12 $/\$
182	55	elsnres 5147	. . . . . . . . . . . . . . 15 $/\$
183	182	anbi1i 709	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
184		19.41v 1838	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
185		anass 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
186	185	exbii 1726	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
187	183, 184, 186	3bitr2i 281	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
188	187	exbii 1726	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
189	181, 188	bitri 257	. . . . . . . . . . 11 $/\$ $/\$
190	180, 189	sylibr 217	. . . . . . . . . 10
191		ssrexv 3480	. . . . . . . . . 10
192	165, 190, 191	mpsyl 64	. . . . . . . . 9
193	164, 192	syl6 33	. . . . . . . 8 $/\$ $/\$ $/\$
194	193	expd 443	. . . . . . 7 $/\$ $/\$
195	194	rexlimdv 2870	. . . . . 6 $/\$ $/\$
196	195	3expib 1234	. . . . 5 $/\$
197	196	adantl 473	. . . 4 $/\$ $/\$
198	33, 197	mpdd 40	. . 3 $/\$ $/\$
199	198	alrimiv 1781	. 2 $/\$ $/\$
200		df-fr 4798	. 2 $/\$
201	199, 200	sylibr 217	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 375 $/\$ wa 376 $/\$ w3a 1007

wal 1450

wceq 1452

wex 1671

wcel 1904

wne 2641

wral 2756

wrex 2757

cvv 3031

wss 3390

c0 3722

csn 3959

cop 3965 class class class wbr 4395

copab 4453

wfr 4795

cxp 4837

cdm 4839

crn 4840

cres 4841

cima 4842

wrel 4844

cfv 5589

c1st 6810

c2nd 6811

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-rab 2765 df-v 3033 df-sbc 3256 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-nul 3723 df-if 3873 df-sn 3960 df-pr 3962 df-op 3966 df-uni 4191 df-int 4227 df-br 4396 df-opab 4455 df-mpt 4456 df-id 4754 df-fr 4798 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-iota 5553 df-fun 5591 df-fv 5597 df-1st 6812 df-2nd 6813

This theorem is referenced by: wexp 6929

W3C validator