frxp - Metamath Proof Explorer

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

Theorem frxp 6915

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 3796	. . . . . . . . 9 $/\$
2		xpnz 5273	. . . . . . . . . . 11 $/\$
3	2	biimpri 210	. . . . . . . . . 10 $/\$
4	3	simprd 465	. . . . . . . . 9
5	1, 4	syl 17	. . . . . . . 8 $/\$
6		dmxp 5070	. . . . . . . . . 10
7		dmss 5051	. . . . . . . . . . 11
8		sseq2 3487	. . . . . . . . . . 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 4959	. . . . . . . . . . 11
14		relss 4939	. . . . . . . . . . 11
15	13, 14	mpi 21	. . . . . . . . . 10
16		reldm0 5069	. . . . . . . . . 10
17	15, 16	syl 17	. . . . . . . . 9
18	17	necon3bid 2683	. . . . . . . 8
19	18	biimpa 487	. . . . . . 7 $/\$
20	12, 19	jca 535	. . . . . 6 $/\$ $/\$
21		df-fr 4810	. . . . . . 7 $/\$
22		vex 3085	. . . . . . . . 9
23	22	dmex 6738	. . . . . . . 8
24		sseq1 3486	. . . . . . . . . 10
25		neeq1 2706	. . . . . . . . . 10
26	24, 25	anbi12d 716	. . . . . . . . 9 $/\$ $/\$
27		raleq 3026	. . . . . . . . . 10
28	27	rexeqbi1dv 3035	. . . . . . . . 9
29	26, 28	imbi12d 322	. . . . . . . 8 $/\$ $/\$
30	23, 29	spcv 3173	. . . . . . 7 $/\$ $/\$
31	21, 30	sylbi 199	. . . . . 6 $/\$
32	20, 31	syl5 34	. . . . 5 $/\$
33	32	adantr 467	. . . 4 $/\$ $/\$
34		imassrn 5196	. . . . . . . . . . . . . . 15
35		xpeq0 5274	. . . . . . . . . . . . . . . . . . . 20 $\/$
36	35	biimpri 210	. . . . . . . . . . . . . . . . . . 19 $\/$
37	36	orcs 396	. . . . . . . . . . . . . . . . . 18
38		sseq2 3487	. . . . . . . . . . . . . . . . . . 19
39		ss0 3794	. . . . . . . . . . . . . . . . . . 19
40	38, 39	syl6bi 232	. . . . . . . . . . . . . . . . . 18
41	37, 40	syl 17	. . . . . . . . . . . . . . . . 17
42		rneq 5077	. . . . . . . . . . . . . . . . . 18
43		rn0 5103	. . . . . . . . . . . . . . . . . . 19
44		0ss 3792	. . . . . . . . . . . . . . . . . . 19
45	43, 44	eqsstri 3495	. . . . . . . . . . . . . . . . . 18
46	42, 45	syl6eqss 3515	. . . . . . . . . . . . . . . . 17
47	41, 46	syl6 35	. . . . . . . . . . . . . . . 16
48		rnxp 5284	. . . . . . . . . . . . . . . . 17
49		rnss 5080	. . . . . . . . . . . . . . . . . 18
50		sseq2 3487	. . . . . . . . . . . . . . . . . 18
51	49, 50	syl5ib 223	. . . . . . . . . . . . . . . . 17
52	48, 51	syl 17	. . . . . . . . . . . . . . . 16
53	47, 52	pm2.61ine 2738	. . . . . . . . . . . . . . 15
54	34, 53	syl5ss 3476	. . . . . . . . . . . . . 14
55		vex 3085	. . . . . . . . . . . . . . . 16
56	55	eldm 5049	. . . . . . . . . . . . . . 15
57		vex 3085	. . . . . . . . . . . . . . . . . . 19
58	55, 57	elimasn 5210	. . . . . . . . . . . . . . . . . 18
59		df-br 4422	. . . . . . . . . . . . . . . . . 18
60	58, 59	bitr4i 256	. . . . . . . . . . . . . . . . 17
61		ne0i 3768	. . . . . . . . . . . . . . . . 17
62	60, 61	sylbir 217	. . . . . . . . . . . . . . . 16
63	62	exlimiv 1767	. . . . . . . . . . . . . . 15
64	56, 63	sylbi 199	. . . . . . . . . . . . . 14
65		df-fr 4810	. . . . . . . . . . . . . . 15 $/\$
66		imaexg 6742	. . . . . . . . . . . . . . . . 17
67	22, 66	ax-mp 5	. . . . . . . . . . . . . . . 16
68		sseq1 3486	. . . . . . . . . . . . . . . . . 18
69		neeq1 2706	. . . . . . . . . . . . . . . . . 18
70	68, 69	anbi12d 716	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
71		raleq 3026	. . . . . . . . . . . . . . . . . 18
72	71	rexeqbi1dv 3035	. . . . . . . . . . . . . . . . 17
73	70, 72	imbi12d 322	. . . . . . . . . . . . . . . 16 $/\$ $/\$
74	67, 73	spcv 3173	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	65, 74	sylbi 199	. . . . . . . . . . . . . 14 $/\$
76	54, 64, 75	syl2ani 661	. . . . . . . . . . . . 13 $/\$
77		1stdm 6852	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
78		breq1 4424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
79	78	notbid 296	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
80	79	rspccv 3180	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
81	77, 80	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
82	81	expd 438	. . . . . . . . . . . . . . . . . . . . . . . . 25
83	82	impcom 432	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
84	83	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
85		elrel 4954	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
86	85	ex 436	. . . . . . . . . . . . . . . . . . . . . . . . . 26
87	86	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
88		vex 3085	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
89	55, 88	elimasn 5210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
90		breq1 4424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
91	90	notbid 296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
92	91	rspccv 3180	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
93	89, 92	syl5bir 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
94	93	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
95		opeq1 4185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
96	95	eleq1d 2492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
97	96	imbi1d 319	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
98	94, 97	syl5ibr 225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
99	98	com3l 85	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
100		eleq1 2495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
101		vex 3085	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
102	101, 88	op1std 6815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
103	102	eqeq1d 2425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
104	101, 88	op2ndd 6816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
105	104	breq1d 4431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1768	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
111	110	com3l 85	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
112	87, 111	mpdd 42	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
113	112	adantlr 720	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
114	84, 113	jcad 536	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
115	114	ralrimiv 2838	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
116	115	ex 436	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
117	15, 116	sylan 474	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
118		olc 386	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\/$ $/\$
119	118	ralimi 2819	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\/$ $/\$
120	117, 119	syl6 35	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\/$ $/\$
121		ianor 491	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$
122		vex 3085	. . . . . . . . . . . . . . . . . . . . . 22
123		opex 4683	. . . . . . . . . . . . . . . . . . . . . 22
124		eleq1 2495	. . . . . . . . . . . . . . . . . . . . . . . 24
125	124	anbi1d 710	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
126		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . 25
127	126	breq1d 4431	. . . . . . . . . . . . . . . . . . . . . . . 24
128	126	eqeq1d 2425	. . . . . . . . . . . . . . . . . . . . . . . . 25
129		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130	129	breq1d 4431	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	128, 130	anbi12d 716	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
132	127, 131	orbi12d 715	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $/\$ $\/$ $/\$
133	125, 132	anbi12d 716	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
134		eleq1 2495	. . . . . . . . . . . . . . . . . . . . . . . 24
135	134	anbi2d 709	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
136	55, 57	op1std 6815	. . . . . . . . . . . . . . . . . . . . . . . . 25
137	136	breq2d 4433	. . . . . . . . . . . . . . . . . . . . . . . 24
138	136	eqeq2d 2437	. . . . . . . . . . . . . . . . . . . . . . . . 25
139	55, 57	op2ndd 6816	. . . . . . . . . . . . . . . . . . . . . . . . . 26
140	139	breq2d 4433	. . . . . . . . . . . . . . . . . . . . . . . . 25
141	138, 140	anbi12d 716	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
142	137, 141	orbi12d 715	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $/\$ $\/$ $/\$
143	135, 142	anbi12d 716	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
144		frxp.1	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$ $/\$
145	122, 123, 133, 143, 144	brab 4741	. . . . . . . . . . . . . . . . . . . . 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 699	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
152	147, 151	bitri 253	. . . . . . . . . . . . . . . . . . . . 21 $\/$ $/\$ $/\$
153	152	orbi2i 522	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$
154	146, 153	bitri 253	. . . . . . . . . . . . . . . . . . 19 $/\$ $\/$ $/\$
155	154	ralbii 2857	. . . . . . . . . . . . . . . . . 18 $/\$ $\/$ $/\$
156	120, 155	syl6ibr 231	. . . . . . . . . . . . . . . . 17 $/\$
157	156	reximdv 2900	. . . . . . . . . . . . . . . 16 $/\$
158	157	ex 436	. . . . . . . . . . . . . . 15
159	158	com23 82	. . . . . . . . . . . . . 14
160	159	adantr 467	. . . . . . . . . . . . 13 $/\$
161	76, 160	sylcom 31	. . . . . . . . . . . 12 $/\$
162	161	impl 625	. . . . . . . . . . 11 $/\$ $/\$
163	162	expimpd 607	. . . . . . . . . 10 $/\$ $/\$
164	163	3adant3 1026	. . . . . . . . 9 $/\$ $/\$ $/\$
165		resss 5145	. . . . . . . . . 10
166		df-rex 2782	. . . . . . . . . . . . 13 $/\$
167		eqid 2423	. . . . . . . . . . . . . . . 16
168		eqeq1 2427	. . . . . . . . . . . . . . . . . 18
169		breq2 4425	. . . . . . . . . . . . . . . . . . . . 21
170	169	notbid 296	. . . . . . . . . . . . . . . . . . . 20
171	170	ralbidv 2865	. . . . . . . . . . . . . . . . . . 19
172	171	anbi2d 709	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
173	168, 172	anbi12d 716	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
174	123, 173	spcev 3174	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
175	167, 174	mpan 675	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
176	58, 175	sylanb 475	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
177	176	eximi 1703	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
178	166, 177	sylbi 199	. . . . . . . . . . . 12 $/\$ $/\$
179		excom 1900	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
180	178, 179	sylib 200	. . . . . . . . . . 11 $/\$ $/\$
181		df-rex 2782	. . . . . . . . . . . 12 $/\$
182	55	elsnres 5158	. . . . . . . . . . . . . . 15 $/\$
183	182	anbi1i 700	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
184		19.41v 1820	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
185		anass 654	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
186	185	exbii 1713	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
187	183, 184, 186	3bitr2i 277	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
188	187	exbii 1713	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
189	181, 188	bitri 253	. . . . . . . . . . 11 $/\$ $/\$
190	180, 189	sylibr 216	. . . . . . . . . 10
191		ssrexv 3527	. . . . . . . . . 10
192	165, 190, 191	mpsyl 66	. . . . . . . . 9
193	164, 192	syl6 35	. . . . . . . 8 $/\$ $/\$ $/\$
194	193	expd 438	. . . . . . 7 $/\$ $/\$
195	194	rexlimdv 2916	. . . . . 6 $/\$ $/\$
196	195	3expib 1209	. . . . 5 $/\$
197	196	adantl 468	. . . 4 $/\$ $/\$
198	33, 197	mpdd 42	. . 3 $/\$ $/\$
199	198	alrimiv 1764	. 2 $/\$ $/\$
200		df-fr 4810	. 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 983

wal 1436

wceq 1438

wex 1660

wcel 1869

wne 2619

wral 2776

wrex 2777

cvv 3082

wss 3437

c0 3762

csn 3997

cop 4003 class class class wbr 4421

copab 4479

wfr 4807

cxp 4849

cdm 4851

crn 4852

cres 4853

cima 4854

wrel 4856

cfv 5599

c1st 6803

c2nd 6804

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-sep 4544 ax-nul 4553 ax-pow 4600 ax-pr 4658 ax-un 6595

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 985 df-tru 1441 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-ral 2781 df-rex 2782 df-rab 2785 df-v 3084 df-sbc 3301 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-nul 3763 df-if 3911 df-sn 3998 df-pr 4000 df-op 4004 df-uni 4218 df-int 4254 df-br 4422 df-opab 4481 df-mpt 4482 df-id 4766 df-fr 4810 df-xp 4857 df-rel 4858 df-cnv 4859 df-co 4860 df-dm 4861 df-rn 4862 df-res 4863 df-ima 4864 df-iota 5563 df-fun 5601 df-fv 5607 df-1st 6805 df-2nd 6806

This theorem is referenced by: wexp 6919

W3C validator