fpwwe2 - Metamath Proof Explorer

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

Theorem fpwwe2 9465

Description: Given any function

from well-orderings of subsets of

, there is a unique well-ordered subset

which "agrees" with

in the sense that each initial segment maps to its upper bound, and such that the entire set maps to an element of the set (so that it cannot be extended without losing the well-ordering). This theorem can be used to prove dfac8a 8853. Theorem 1.1 of [KanamoriPincus] p. 415. (Contributed by Mario Carneiro, 18-May-2015.)

**Hypotheses**
Ref	Expression
fpwwe2.1	$/\$ $/\$ $/\$
fpwwe2.2
fpwwe2.3	$/\$ $/\$ $/\$
fpwwe2.4

**Assertion**
Ref	Expression
fpwwe2	$/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

Proof of Theorem fpwwe2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fpwwe2.1	. . . . . . . . . . 11 $/\$ $/\$ $/\$
2		fpwwe2.2	. . . . . . . . . . 11
3		fpwwe2.3	. . . . . . . . . . 11 $/\$ $/\$ $/\$
4		fpwwe2.4	. . . . . . . . . . 11
5	1, 2, 3, 4	fpwwe2lem11 9462	. . . . . . . . . 10
6		ffun 6048	. . . . . . . . . 10
7	5, 6	syl 17	. . . . . . . . 9
8		funbrfv2b 6240	. . . . . . . . 9 $/\$
9	7, 8	syl 17	. . . . . . . 8 $/\$
10	9	simprbda 653	. . . . . . 7 $/\$
11	10	adantrr 753	. . . . . 6 $/\$ $/\$
12		elssuni 4467	. . . . . . 7
13	12, 4	syl6sseqr 3652	. . . . . 6
14	11, 13	syl 17	. . . . 5 $/\$ $/\$
15		simpl 473	. . . . . . 7 $/\$
16	15	a1i 11	. . . . . 6 $/\$ $/\$ $/\$
17		simplrr 801	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
18	2	adantr 481	. . . . . . . . . . . . . . 15 $/\$ $/\$
19	18	adantr 481	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
20	1, 2, 3, 4	fpwwe2lem12 9463	. . . . . . . . . . . . . . . . . . 19
21		funfvbrb 6330	. . . . . . . . . . . . . . . . . . . 20
22	7, 21	syl 17	. . . . . . . . . . . . . . . . . . 19
23	20, 22	mpbid 222	. . . . . . . . . . . . . . . . . 18
24	1, 2	fpwwe2lem2 9454	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
25	23, 24	mpbid 222	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
26	25	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27	26	simpld 475	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
28	27	simpld 475	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
29	19, 28	ssexd 4805	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
30		difexg 4808	. . . . . . . . . . . . 13 $\$
31	29, 30	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $\$
32	26	simprd 479	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
33	32	simpld 475	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
34		wefr 5104	. . . . . . . . . . . . 13
35	33, 34	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
36		difssd 3738	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $\$
37		fri 5076	. . . . . . . . . . . . 13 $\$ $/\$ $/\$ $\$ $/\$ $\$ $\$ $\$
38	37	expr 643	. . . . . . . . . . . 12 $\$ $/\$ $/\$ $\$ $\$ $\$ $\$
39	31, 35, 36, 38	syl21anc 1325	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
40		ssdif0 3942	. . . . . . . . . . . . . . 15 $\$
41		indif1 3871	. . . . . . . . . . . . . . . 16 $\$ $\$
42	41	eqeq1i 2627	. . . . . . . . . . . . . . 15 $\$ $\$
43		disj 4017	. . . . . . . . . . . . . . . 16 $\$ $\$
44		vex 3203	. . . . . . . . . . . . . . . . . . 19
45		vex 3203	. . . . . . . . . . . . . . . . . . . 20
46	45	eliniseg 5494	. . . . . . . . . . . . . . . . . . 19
47	44, 46	ax-mp 5	. . . . . . . . . . . . . . . . . 18
48	47	notbii 310	. . . . . . . . . . . . . . . . 17
49	48	ralbii 2980	. . . . . . . . . . . . . . . 16 $\$ $\$
50	43, 49	bitri 264	. . . . . . . . . . . . . . 15 $\$ $\$
51	40, 42, 50	3bitr2i 288	. . . . . . . . . . . . . 14 $\$
52		cnvimass 5485	. . . . . . . . . . . . . . . . 17
53	27	simprd 479	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
54		dmss 5323	. . . . . . . . . . . . . . . . . . 19
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
56		dmxpid 5345	. . . . . . . . . . . . . . . . . 18
57	55, 56	syl6sseq 3651	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
58	52, 57	syl5ss 3614	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
59		sseqin2 3817	. . . . . . . . . . . . . . . 16
60	58, 59	sylib 208	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
61	60	sseq1d 3632	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
62	51, 61	syl5bbr 274	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$
63	62	rexbidv 3052	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$
64		eldifn 3733	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
65	64	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
66		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . 25
67	66	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . 24
68	65, 67	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
69	68	con2d 129	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
70	69	imp 445	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
71	65	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
72		simprr 796	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
73	72	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
74	73	breqd 4664	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
75		eldifi 3732	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
76	75	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
77	76	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
78		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
79		brxp 5147	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
80	77, 78, 79	sylanbrc 698	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
81		brin 4704	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
82	81	rbaib 947	. . . . . . . . . . . . . . . . . . . . . . . . 25
83	80, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
84	74, 83	bitrd 268	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
85	1, 2	fpwwe2lem2 9454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
86	85	biimpa 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
87	86	adantrr 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
88	87	simpld 475	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
89	88	simprd 479	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
90	89	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
91	90	ssbrd 4696	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
92		brxp 5147	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
93	92	simplbi 476	. . . . . . . . . . . . . . . . . . . . . . . 24
94	91, 93	syl6 35	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
95	84, 94	sylbird 250	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
96	71, 95	mtod 189	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
97	33	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
98		weso 5105	. . . . . . . . . . . . . . . . . . . . . . 23
99	97, 98	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
100	14	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
101	100	sselda 3603	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
102		sotric 5061	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\/$
103		ioran 511	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $/\$
104	102, 103	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
105	99, 101, 77, 104	syl12anc 1324	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
106	70, 96, 105	mpbir2and 957	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
107	106, 47	sylibr 224	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
108	107	ex 450	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
109	108	ssrdv 3609	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
110		simprr 796	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
111	109, 110	eqssd 3620	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
112		in32 3825	. . . . . . . . . . . . . . . . . 18
113		simplrr 801	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
114	113	ineq1d 3813	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
115	89	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
116		df-ss 3588	. . . . . . . . . . . . . . . . . . . 20
117	115, 116	sylib 208	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
118	114, 117	eqtr3d 2658	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
119		inss2 3834	. . . . . . . . . . . . . . . . . . . 20
120		xpss1 5228	. . . . . . . . . . . . . . . . . . . . 21
121	100, 120	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
122	119, 121	syl5ss 3614	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
123		df-ss 3588	. . . . . . . . . . . . . . . . . . 19
124	122, 123	sylib 208	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
125	112, 118, 124	3eqtr3a 2680	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
126	111	sqxpeqd 5141	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
127	126	ineq2d 3814	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
128	125, 127	eqtrd 2656	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
129	111, 128	oveq12d 6668	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
130	19	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
131	23	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
132	131	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
133	1, 130, 132	fpwwe2lem3 9455	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
134	76, 133	mpdan 702	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
135	129, 134	eqtrd 2656	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
136	135, 65	eqneltrd 2720	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
137	136	rexlimdvaa 3032	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $\$
138	63, 137	sylbid 230	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $\$ $\$
139	39, 138	syld 47	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $\$
140	139	necon4ad 2813	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\$
141	17, 140	mpd 15	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\$
142		ssdif0 3942	. . . . . . . 8 $\$
143	141, 142	sylibr 224	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
144	143	ex 450	. . . . . 6 $/\$ $/\$ $/\$
145	3	adantlr 751	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
146		simprl 794	. . . . . . 7 $/\$ $/\$
147	1, 18, 145, 131, 146	fpwwe2lem10 9461	. . . . . 6 $/\$ $/\$ $/\$ $\/$ $/\$
148	16, 144, 147	mpjaod 396	. . . . 5 $/\$ $/\$
149	14, 148	eqssd 3620	. . . 4 $/\$ $/\$
150	7	adantr 481	. . . . . 6 $/\$ $/\$
151	149, 146	eqbrtrrd 4677	. . . . . 6 $/\$ $/\$
152		funbrfv 6234	. . . . . 6
153	150, 151, 152	sylc 65	. . . . 5 $/\$ $/\$
154	153	eqcomd 2628	. . . 4 $/\$ $/\$
155	149, 154	jca 554	. . 3 $/\$ $/\$ $/\$
156	155	ex 450	. 2 $/\$ $/\$
157	1, 2, 3, 4	fpwwe2lem13 9464	. . . 4
158	23, 157	jca 554	. . 3 $/\$
159		breq12 4658	. . . 4 $/\$
160		oveq12 6659	. . . . 5 $/\$
161		simpl 473	. . . . 5 $/\$
162	160, 161	eleq12d 2695	. . . 4 $/\$
163	159, 162	anbi12d 747	. . 3 $/\$ $/\$ $/\$
164	158, 163	syl5ibrcom 237	. 2 $/\$ $/\$
165	156, 164	impbid 202	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990

wne 2794

wral 2912

wrex 2913

cvv 3200

wsbc 3435 $\$ cdif 3571

cin 3573

wss 3574

c0 3915

cpw 4158

csn 4177

cuni 4436 class class class wbr 4653

copab 4712

wor 5034

wfr 5070

wwe 5072

cxp 5112

ccnv 5113

cdm 5114

cima 5117

wfun 5882

wf 5884

cfv 5888 (class class class)co 6650

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-wrecs 7407 df-recs 7468 df-oi 8415

This theorem is referenced by: fpwwe 9468 canthwelem 9472 pwfseqlem4 9484

W3C validator