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 6906

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 3767	. . . . . . . . 9 $/\$
2		xpnz 5256	. . . . . . . . . . 11 $/\$
3	2	biimpri 210	. . . . . . . . . 10 $/\$
4	3	simprd 465	. . . . . . . . 9
5	1, 4	syl 17	. . . . . . . 8 $/\$
6		dmxp 5053	. . . . . . . . . 10
7		dmss 5034	. . . . . . . . . . 11
8		sseq2 3454	. . . . . . . . . . 11
9	7, 8	syl5ib 223	. . . . . . . . . 10
10	6, 9	syl 17	. . . . . . . . 9
11	10	impcom 432	. . . . . . . 8 $/\$
12	5, 11	syldan 473	. . . . . . 7 $/\$
13		relxp 4942	. . . . . . . . . . 11
14		relss 4922	. . . . . . . . . . 11
15	13, 14	mpi 20	. . . . . . . . . 10
16		reldm0 5052	. . . . . . . . . 10
17	15, 16	syl 17	. . . . . . . . 9
18	17	necon3bid 2668	. . . . . . . 8
19	18	biimpa 487	. . . . . . 7 $/\$
20	12, 19	jca 535	. . . . . 6 $/\$ $/\$
21		df-fr 4793	. . . . . . 7 $/\$
22		vex 3048	. . . . . . . . 9
23	22	dmex 6726	. . . . . . . 8
24		sseq1 3453	. . . . . . . . . 10
25		neeq1 2686	. . . . . . . . . 10
26	24, 25	anbi12d 717	. . . . . . . . 9 $/\$ $/\$
27		raleq 2987	. . . . . . . . . 10
28	27	rexeqbi1dv 2996	. . . . . . . . 9
29	26, 28	imbi12d 322	. . . . . . . 8 $/\$ $/\$
30	23, 29	spcv 3140	. . . . . . 7 $/\$ $/\$
31	21, 30	sylbi 199	. . . . . 6 $/\$
32	20, 31	syl5 33	. . . . 5 $/\$
33	32	adantr 467	. . . 4 $/\$ $/\$
34		imassrn 5179	. . . . . . . . . . . . . . 15
35		xpeq0 5257	. . . . . . . . . . . . . . . . . . . 20 $\/$
36	35	biimpri 210	. . . . . . . . . . . . . . . . . . 19 $\/$
37	36	orcs 396	. . . . . . . . . . . . . . . . . 18
38		sseq2 3454	. . . . . . . . . . . . . . . . . . 19
39		ss0 3765	. . . . . . . . . . . . . . . . . . 19
40	38, 39	syl6bi 232	. . . . . . . . . . . . . . . . . 18
41	37, 40	syl 17	. . . . . . . . . . . . . . . . 17
42		rneq 5060	. . . . . . . . . . . . . . . . . 18
43		rn0 5086	. . . . . . . . . . . . . . . . . . 19
44		0ss 3763	. . . . . . . . . . . . . . . . . . 19
45	43, 44	eqsstri 3462	. . . . . . . . . . . . . . . . . 18
46	42, 45	syl6eqss 3482	. . . . . . . . . . . . . . . . 17
47	41, 46	syl6 34	. . . . . . . . . . . . . . . 16
48		rnxp 5267	. . . . . . . . . . . . . . . . 17
49		rnss 5063	. . . . . . . . . . . . . . . . . 18
50		sseq2 3454	. . . . . . . . . . . . . . . . . 18
51	49, 50	syl5ib 223	. . . . . . . . . . . . . . . . 17
52	48, 51	syl 17	. . . . . . . . . . . . . . . 16
53	47, 52	pm2.61ine 2707	. . . . . . . . . . . . . . 15
54	34, 53	syl5ss 3443	. . . . . . . . . . . . . 14
55		vex 3048	. . . . . . . . . . . . . . . 16
56	55	eldm 5032	. . . . . . . . . . . . . . 15
57		vex 3048	. . . . . . . . . . . . . . . . . . 19
58	55, 57	elimasn 5193	. . . . . . . . . . . . . . . . . 18
59		df-br 4403	. . . . . . . . . . . . . . . . . 18
60	58, 59	bitr4i 256	. . . . . . . . . . . . . . . . 17
61		ne0i 3737	. . . . . . . . . . . . . . . . 17
62	60, 61	sylbir 217	. . . . . . . . . . . . . . . 16
63	62	exlimiv 1776	. . . . . . . . . . . . . . 15
64	56, 63	sylbi 199	. . . . . . . . . . . . . 14
65		df-fr 4793	. . . . . . . . . . . . . . 15 $/\$
66		imaexg 6730	. . . . . . . . . . . . . . . . 17
67	22, 66	ax-mp 5	. . . . . . . . . . . . . . . 16
68		sseq1 3453	. . . . . . . . . . . . . . . . . 18
69		neeq1 2686	. . . . . . . . . . . . . . . . . 18
70	68, 69	anbi12d 717	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
71		raleq 2987	. . . . . . . . . . . . . . . . . 18
72	71	rexeqbi1dv 2996	. . . . . . . . . . . . . . . . 17
73	70, 72	imbi12d 322	. . . . . . . . . . . . . . . 16 $/\$ $/\$
74	67, 73	spcv 3140	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	65, 74	sylbi 199	. . . . . . . . . . . . . 14 $/\$
76	54, 64, 75	syl2ani 662	. . . . . . . . . . . . 13 $/\$
77		1stdm 6840	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
78		breq1 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
79	78	notbid 296	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
80	79	rspccv 3147	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
81	77, 80	syl5 33	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
82	81	expd 438	. . . . . . . . . . . . . . . . . . . . . . . . 25
83	82	impcom 432	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
84	83	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
85		elrel 4937	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
86	85	ex 436	. . . . . . . . . . . . . . . . . . . . . . . . . 26
87	86	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
88		vex 3048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
89	55, 88	elimasn 5193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
90		breq1 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
91	90	notbid 296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
92	91	rspccv 3147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
93	89, 92	syl5bir 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
94	93	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
95		opeq1 4166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
96	95	eleq1d 2513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
97	96	imbi1d 319	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
98	94, 97	syl5ibr 225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
99	98	com3l 84	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
100		eleq1 2517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101		vex 3048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
102	101, 88	op1std 6803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
103	102	eqeq1d 2453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
104	101, 88	op2ndd 6804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
105	104	breq1d 4412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106	105	notbid 296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
107	103, 106	imbi12d 322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
108	100, 107	imbi12d 322	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
109	99, 108	syl5ibr 225	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
110	109	exlimivv 1778	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
111	110	com3l 84	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
112	87, 111	mpdd 41	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
113	112	adantlr 721	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
114	84, 113	jcad 536	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
115	114	ralrimiv 2800	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
116	115	ex 436	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
117	15, 116	sylan 474	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
118		olc 386	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\/$ $/\$
119	118	ralimi 2781	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\/$ $/\$
120	117, 119	syl6 34	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\/$ $/\$
121		ianor 491	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$
122		vex 3048	. . . . . . . . . . . . . . . . . . . . . 22
123		opex 4664	. . . . . . . . . . . . . . . . . . . . . 22
124		eleq1 2517	. . . . . . . . . . . . . . . . . . . . . . . 24
125	124	anbi1d 711	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
126		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . . . 25
127	126	breq1d 4412	. . . . . . . . . . . . . . . . . . . . . . . 24
128	126	eqeq1d 2453	. . . . . . . . . . . . . . . . . . . . . . . . 25
129		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130	129	breq1d 4412	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	128, 130	anbi12d 717	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
132	127, 131	orbi12d 716	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $/\$ $\/$ $/\$
133	125, 132	anbi12d 717	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
134		eleq1 2517	. . . . . . . . . . . . . . . . . . . . . . . 24
135	134	anbi2d 710	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
136	55, 57	op1std 6803	. . . . . . . . . . . . . . . . . . . . . . . . 25
137	136	breq2d 4414	. . . . . . . . . . . . . . . . . . . . . . . 24
138	136	eqeq2d 2461	. . . . . . . . . . . . . . . . . . . . . . . . 25
139	55, 57	op2ndd 6804	. . . . . . . . . . . . . . . . . . . . . . . . . 26
140	139	breq2d 4414	. . . . . . . . . . . . . . . . . . . . . . . . 25
141	138, 140	anbi12d 717	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
142	137, 141	orbi12d 716	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $/\$ $\/$ $/\$
143	135, 142	anbi12d 717	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
144		frxp.1	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$
145	122, 123, 133, 143, 144	brab 4724	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\/$ $/\$
146	121, 145	xchnxbir 311	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\/$ $\/$ $/\$
147		ioran 493	. . . . . . . . . . . . . . . . . . . . . 22 $\/$ $/\$ $/\$ $/\$
148		ianor 491	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\/$
149		pm4.62 421	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
150	148, 149	bitr4i 256	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
151	150	anbi2i 700	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
152	147, 151	bitri 253	. . . . . . . . . . . . . . . . . . . . 21 $\/$ $/\$ $/\$
153	152	orbi2i 522	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$
154	146, 153	bitri 253	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$ $/\$
155	154	ralbii 2819	. . . . . . . . . . . . . . . . . 18 $/\$ $\/$ $/\$
156	120, 155	syl6ibr 231	. . . . . . . . . . . . . . . . 17 $/\$
157	156	reximdv 2861	. . . . . . . . . . . . . . . 16 $/\$
158	157	ex 436	. . . . . . . . . . . . . . 15
159	158	com23 81	. . . . . . . . . . . . . 14
160	159	adantr 467	. . . . . . . . . . . . 13 $/\$
161	76, 160	sylcom 30	. . . . . . . . . . . 12 $/\$
162	161	impl 626	. . . . . . . . . . 11 $/\$ $/\$
163	162	expimpd 608	. . . . . . . . . 10 $/\$ $/\$
164	163	3adant3 1028	. . . . . . . . 9 $/\$ $/\$ $/\$
165		resss 5128	. . . . . . . . . 10
166		df-rex 2743	. . . . . . . . . . . . 13 $/\$
167		eqid 2451	. . . . . . . . . . . . . . . 16
168		eqeq1 2455	. . . . . . . . . . . . . . . . . 18
169		breq2 4406	. . . . . . . . . . . . . . . . . . . . 21
170	169	notbid 296	. . . . . . . . . . . . . . . . . . . 20
171	170	ralbidv 2827	. . . . . . . . . . . . . . . . . . 19
172	171	anbi2d 710	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
173	168, 172	anbi12d 717	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
174	123, 173	spcev 3141	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
175	167, 174	mpan 676	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
176	58, 175	sylanb 475	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
177	176	eximi 1707	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
178	166, 177	sylbi 199	. . . . . . . . . . . 12 $/\$ $/\$
179		excom 1927	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
180	178, 179	sylib 200	. . . . . . . . . . 11 $/\$ $/\$
181		df-rex 2743	. . . . . . . . . . . 12 $/\$
182	55	elsnres 5141	. . . . . . . . . . . . . . 15 $/\$
183	182	anbi1i 701	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
184		19.41v 1830	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
185		anass 655	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
186	185	exbii 1718	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
187	183, 184, 186	3bitr2i 277	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
188	187	exbii 1718	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
189	181, 188	bitri 253	. . . . . . . . . . 11 $/\$ $/\$
190	180, 189	sylibr 216	. . . . . . . . . 10
191		ssrexv 3494	. . . . . . . . . 10
192	165, 190, 191	mpsyl 65	. . . . . . . . 9
193	164, 192	syl6 34	. . . . . . . 8 $/\$ $/\$ $/\$
194	193	expd 438	. . . . . . 7 $/\$ $/\$
195	194	rexlimdv 2877	. . . . . 6 $/\$ $/\$
196	195	3expib 1211	. . . . 5 $/\$
197	196	adantl 468	. . . 4 $/\$ $/\$
198	33, 197	mpdd 41	. . 3 $/\$ $/\$
199	198	alrimiv 1773	. 2 $/\$ $/\$
200		df-fr 4793	. 2 $/\$
201	199, 200	sylibr 216	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371 $/\$ w3a 985

wal 1442

wceq 1444

wex 1663

wcel 1887

wne 2622

wral 2737

wrex 2738

cvv 3045

wss 3404

c0 3731

csn 3968

cop 3974 class class class wbr 4402

copab 4460

wfr 4790

cxp 4832

cdm 4834

crn 4835

cres 4836

cima 4837

wrel 4839

cfv 5582

c1st 6791

c2nd 6792

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-ral 2742 df-rex 2743 df-rab 2746 df-v 3047 df-sbc 3268 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-nul 3732 df-if 3882 df-sn 3969 df-pr 3971 df-op 3975 df-uni 4199 df-int 4235 df-br 4403 df-opab 4462 df-mpt 4463 df-id 4749 df-fr 4793 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-iota 5546 df-fun 5584 df-fv 5590 df-1st 6793 df-2nd 6794

This theorem is referenced by: wexp 6910

W3C validator