frxp - Metamath Proof Explorer

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

Theorem frxp 6681

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 3667	. . . . . . . . 9 $/\$
2		xpnz 5254	. . . . . . . . . . 11 $/\$
3	2	biimpri 206	. . . . . . . . . 10 $/\$
4	3	simprd 460	. . . . . . . . 9
5	1, 4	syl 16	. . . . . . . 8 $/\$
6		dmxp 5054	. . . . . . . . . 10
7		dmss 5035	. . . . . . . . . . 11
8		sseq2 3375	. . . . . . . . . . 11
9	7, 8	syl5ib 219	. . . . . . . . . 10
10	6, 9	syl 16	. . . . . . . . 9
11	10	impcom 430	. . . . . . . 8 $/\$
12	5, 11	syldan 467	. . . . . . 7 $/\$
13		relxp 4943	. . . . . . . . . . 11
14		relss 4923	. . . . . . . . . . 11
15	13, 14	mpi 17	. . . . . . . . . 10
16		reldm0 5053	. . . . . . . . . 10
17	15, 16	syl 16	. . . . . . . . 9
18	17	necon3bid 2641	. . . . . . . 8
19	18	biimpa 481	. . . . . . 7 $/\$
20	12, 19	jca 529	. . . . . 6 $/\$ $/\$
21		df-fr 4675	. . . . . . 7 $/\$
22		vex 2973	. . . . . . . . 9
23	22	dmex 6510	. . . . . . . 8
24		sseq1 3374	. . . . . . . . . 10
25		neeq1 2614	. . . . . . . . . 10
26	24, 25	anbi12d 705	. . . . . . . . 9 $/\$ $/\$
27		raleq 2915	. . . . . . . . . 10
28	27	rexeqbi1dv 2924	. . . . . . . . 9
29	26, 28	imbi12d 320	. . . . . . . 8 $/\$ $/\$
30	23, 29	spcv 3060	. . . . . . 7 $/\$ $/\$
31	21, 30	sylbi 195	. . . . . 6 $/\$
32	20, 31	syl5 32	. . . . 5 $/\$
33	32	adantr 462	. . . 4 $/\$ $/\$
34		imassrn 5177	. . . . . . . . . . . . . . 15
35		xpeq0 5255	. . . . . . . . . . . . . . . . . . . 20 $\/$
36	35	biimpri 206	. . . . . . . . . . . . . . . . . . 19 $\/$
37	36	orcs 394	. . . . . . . . . . . . . . . . . 18
38		sseq2 3375	. . . . . . . . . . . . . . . . . . 19
39		ss0 3665	. . . . . . . . . . . . . . . . . . 19
40	38, 39	syl6bi 228	. . . . . . . . . . . . . . . . . 18
41	37, 40	syl 16	. . . . . . . . . . . . . . . . 17
42		rneq 5061	. . . . . . . . . . . . . . . . . 18
43		rn0 5087	. . . . . . . . . . . . . . . . . . 19
44		0ss 3663	. . . . . . . . . . . . . . . . . . 19
45	43, 44	eqsstri 3383	. . . . . . . . . . . . . . . . . 18
46	42, 45	syl6eqss 3403	. . . . . . . . . . . . . . . . 17
47	41, 46	syl6 33	. . . . . . . . . . . . . . . 16
48		rnxp 5265	. . . . . . . . . . . . . . . . 17
49		rnss 5064	. . . . . . . . . . . . . . . . . 18
50		sseq2 3375	. . . . . . . . . . . . . . . . . 18
51	49, 50	syl5ib 219	. . . . . . . . . . . . . . . . 17
52	48, 51	syl 16	. . . . . . . . . . . . . . . 16
53	47, 52	pm2.61ine 2685	. . . . . . . . . . . . . . 15
54	34, 53	syl5ss 3364	. . . . . . . . . . . . . 14
55		vex 2973	. . . . . . . . . . . . . . . 16
56	55	eldm 5033	. . . . . . . . . . . . . . 15
57		vex 2973	. . . . . . . . . . . . . . . . . . 19
58	55, 57	elimasn 5191	. . . . . . . . . . . . . . . . . 18
59		df-br 4290	. . . . . . . . . . . . . . . . . 18
60	58, 59	bitr4i 252	. . . . . . . . . . . . . . . . 17
61		ne0i 3640	. . . . . . . . . . . . . . . . 17
62	60, 61	sylbir 213	. . . . . . . . . . . . . . . 16
63	62	exlimiv 1693	. . . . . . . . . . . . . . 15
64	56, 63	sylbi 195	. . . . . . . . . . . . . 14
65		df-fr 4675	. . . . . . . . . . . . . . 15 $/\$
66		imaexg 6514	. . . . . . . . . . . . . . . . 17
67	22, 66	ax-mp 5	. . . . . . . . . . . . . . . 16
68		sseq1 3374	. . . . . . . . . . . . . . . . . 18
69		neeq1 2614	. . . . . . . . . . . . . . . . . 18
70	68, 69	anbi12d 705	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
71		raleq 2915	. . . . . . . . . . . . . . . . . 18
72	71	rexeqbi1dv 2924	. . . . . . . . . . . . . . . . 17
73	70, 72	imbi12d 320	. . . . . . . . . . . . . . . 16 $/\$ $/\$
74	67, 73	spcv 3060	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	65, 74	sylbi 195	. . . . . . . . . . . . . 14 $/\$
76	54, 64, 75	syl2ani 651	. . . . . . . . . . . . 13 $/\$
77		1stdm 6620	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
78		breq1 4292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
79	78	notbid 294	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
80	79	rspccv 3067	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
81	77, 80	syl5 32	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
82	81	exp3a 436	. . . . . . . . . . . . . . . . . . . . . . . . 25
83	82	impcom 430	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
84	83	adantr 462	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
85		elrel 4938	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
86	85	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . 26
87	86	adantr 462	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
88		vex 2973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
89	55, 88	elimasn 5191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
90		breq1 4292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
91	90	notbid 294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
92	91	rspccv 3067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
93	89, 92	syl5bir 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
94	93	adantl 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
95		opeq1 4056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
96	95	eleq1d 2507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
97	96	imbi1d 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
98	94, 97	syl5ibr 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
99	98	com3l 81	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
100		eleq1 2501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101		vex 2973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
102	101, 88	op1std 6586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
103	102	eqeq1d 2449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
104	101, 88	op2ndd 6587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
105	104	breq1d 4299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1694	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
111	110	com3l 81	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
112	87, 111	mpdd 40	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
113	112	adantlr 709	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
114	84, 113	jcad 530	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
115	114	ralrimiv 2796	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
116	115	ex 434	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
117	15, 116	sylan 468	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
118		olc 384	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\/$ $/\$
119	118	ralimi 2789	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\/$ $/\$
120	117, 119	syl6 33	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\/$ $/\$
121		ianor 485	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$
122		vex 2973	. . . . . . . . . . . . . . . . . . . . . 22
123		opex 4553	. . . . . . . . . . . . . . . . . . . . . 22
124		eleq1 2501	. . . . . . . . . . . . . . . . . . . . . . . 24
125	124	anbi1d 699	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
126		fveq2 5688	. . . . . . . . . . . . . . . . . . . . . . . . 25
127	126	breq1d 4299	. . . . . . . . . . . . . . . . . . . . . . . 24
128	126	eqeq1d 2449	. . . . . . . . . . . . . . . . . . . . . . . . 25
129		fveq2 5688	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130	129	breq1d 4299	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	128, 130	anbi12d 705	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
132	127, 131	orbi12d 704	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $/\$ $\/$ $/\$
133	125, 132	anbi12d 705	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
134		eleq1 2501	. . . . . . . . . . . . . . . . . . . . . . . 24
135	134	anbi2d 698	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
136	55, 57	op1std 6586	. . . . . . . . . . . . . . . . . . . . . . . . 25
137	136	breq2d 4301	. . . . . . . . . . . . . . . . . . . . . . . 24
138	136	eqeq2d 2452	. . . . . . . . . . . . . . . . . . . . . . . . 25
139	55, 57	op2ndd 6587	. . . . . . . . . . . . . . . . . . . . . . . . . 26
140	139	breq2d 4301	. . . . . . . . . . . . . . . . . . . . . . . . 25
141	138, 140	anbi12d 705	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
142	137, 141	orbi12d 704	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $/\$ $\/$ $/\$
143	135, 142	anbi12d 705	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
144		frxp.1	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$
145	122, 123, 133, 143, 144	brab 4609	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\/$ $/\$
146	121, 145	xchnxbir 309	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\/$ $\/$ $/\$
147		ioran 487	. . . . . . . . . . . . . . . . . . . . . 22 $\/$ $/\$ $/\$ $/\$
148		ianor 485	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\/$
149		pm4.62 419	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
150	148, 149	bitr4i 252	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
151	150	anbi2i 689	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
152	147, 151	bitri 249	. . . . . . . . . . . . . . . . . . . . 21 $\/$ $/\$ $/\$
153	152	orbi2i 516	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$
154	146, 153	bitri 249	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$ $/\$
155	154	ralbii 2737	. . . . . . . . . . . . . . . . . 18 $/\$ $\/$ $/\$
156	120, 155	syl6ibr 227	. . . . . . . . . . . . . . . . 17 $/\$
157	156	reximdv 2825	. . . . . . . . . . . . . . . 16 $/\$
158	157	ex 434	. . . . . . . . . . . . . . 15
159	158	com23 78	. . . . . . . . . . . . . 14
160	159	adantr 462	. . . . . . . . . . . . 13 $/\$
161	76, 160	sylcom 29	. . . . . . . . . . . 12 $/\$
162	161	impl 617	. . . . . . . . . . 11 $/\$ $/\$
163	162	expimpd 600	. . . . . . . . . 10 $/\$ $/\$
164	163	3adant3 1003	. . . . . . . . 9 $/\$ $/\$ $/\$
165		resss 5131	. . . . . . . . . 10
166		df-rex 2719	. . . . . . . . . . . . 13 $/\$
167		eqid 2441	. . . . . . . . . . . . . . . 16
168		eqeq1 2447	. . . . . . . . . . . . . . . . . 18
169		breq2 4293	. . . . . . . . . . . . . . . . . . . . 21
170	169	notbid 294	. . . . . . . . . . . . . . . . . . . 20
171	170	ralbidv 2733	. . . . . . . . . . . . . . . . . . 19
172	171	anbi2d 698	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
173	168, 172	anbi12d 705	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
174	123, 173	spcev 3061	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
175	167, 174	mpan 665	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
176	58, 175	sylanb 469	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
177	176	eximi 1630	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
178	166, 177	sylbi 195	. . . . . . . . . . . 12 $/\$ $/\$
179		excom 1792	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
180	178, 179	sylib 196	. . . . . . . . . . 11 $/\$ $/\$
181		df-rex 2719	. . . . . . . . . . . 12 $/\$
182	55	elsnres 5143	. . . . . . . . . . . . . . 15 $/\$
183	182	anbi1i 690	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
184		19.41v 1924	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
185		anass 644	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
186	185	exbii 1639	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
187	183, 184, 186	3bitr2i 273	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
188	187	exbii 1639	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
189	181, 188	bitri 249	. . . . . . . . . . 11 $/\$ $/\$
190	180, 189	sylibr 212	. . . . . . . . . 10
191		ssrexv 3414	. . . . . . . . . 10
192	165, 190, 191	mpsyl 63	. . . . . . . . 9
193	164, 192	syl6 33	. . . . . . . 8 $/\$ $/\$ $/\$
194	193	exp3a 436	. . . . . . 7 $/\$ $/\$
195	194	rexlimdv 2838	. . . . . 6 $/\$ $/\$
196	195	3expib 1185	. . . . 5 $/\$
197	196	adantl 463	. . . 4 $/\$ $/\$
198	33, 197	mpdd 40	. . 3 $/\$ $/\$
199	198	alrimiv 1690	. 2 $/\$ $/\$
200		df-fr 4675	. 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 960

wal 1362

wceq 1364

wex 1591

wcel 1761

wne 2604

wral 2713

wrex 2714

cvv 2970

wss 3325

c0 3634

csn 3874

cop 3880 class class class wbr 4289

copab 4346

wfr 4672

cxp 4834

cdm 4836

crn 4837

cres 4838

cima 4839

wrel 4841

cfv 5415

c1st 6574

c2nd 6575

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2261 df-mo 2262 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-ral 2718 df-rex 2719 df-rab 2722 df-v 2972 df-sbc 3184 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-nul 3635 df-if 3789 df-sn 3875 df-pr 3877 df-op 3881 df-uni 4089 df-int 4126 df-br 4290 df-opab 4348 df-mpt 4349 df-id 4632 df-fr 4675 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fv 5423 df-1st 6576 df-2nd 6577

This theorem is referenced by: wexp 6685

W3C validator