Theorem fpwwe 8900

Description: Given any function F from the powerset of A to A, canth2 7550 gives that the function is not injective, but we can say rather more than that. There is a unique well-ordered subset <. X , ( W ` X ) >. which "agrees" with F 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 8287. Theorem 1.1 of [KanamoriPincus] p. 415. (Contributed by Mario Carneiro, 18-May-2015.)

Hypotheses

Ref	Expression
fpwwe.1	|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) ) }
fpwwe.2	|- ( ph -> A e. _V )
fpwwe.3	|- ( ( ph /\ x e. ( ~P A i^i dom card ) ) -> ( F ` x ) e. A )
fpwwe.4	|- X = U. dom W

Assertion

Ref	Expression
fpwwe	|- ( ph -> ( ( Y W R /\ ( F ` Y ) e. Y ) <-> ( Y = X /\ R = ( W ` X ) ) ) )

Distinct variable groups:   x, r, A   y, r, F, x   ph, r, x, y   R, r, x, y   X, r, x, y   Y, r, x, y   W, r, x, y

Allowed substitution hint:   A( y)

Proof of Theorem fpwwe

Dummy variable u is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ov 6179	. . . . . 6 |- ( Y ( F o. 1st ) R ) = ( ( F o. 1st ) ` <. Y , R >. )
2		fo1st 6682	. . . . . . . 8 |- 1st : _V -onto-> _V
3		fofn 5706	. . . . . . . 8 |- ( 1st : _V -onto-> _V -> 1st Fn _V )
4	2, 3	ax-mp 5	. . . . . . 7 |- 1st Fn _V
5		opex 4640	. . . . . . 7 |- <. Y , R >. e. _V
6		fvco2 5851	. . . . . . 7 |- ( ( 1st Fn _V /\ <. Y , R >. e. _V ) -> ( ( F o. 1st ) ` <. Y , R >. ) = ( F ` ( 1st ` <. Y , R >. ) ) )
7	4, 5, 6	mp2an 672	. . . . . 6 |- ( ( F o. 1st ) ` <. Y , R >. ) = ( F ` ( 1st ` <. Y , R >. ) )
8	1, 7	eqtri 2478	. . . . 5 |- ( Y ( F o. 1st ) R ) = ( F ` ( 1st ` <. Y , R >. ) )
9		fpwwe.1	. . . . . . . . 9 |- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) ) }
10	9	relopabi 5049	. . . . . . . 8 |- Rel W
11		brrelex12 4960	. . . . . . . 8 |- ( ( Rel W /\ Y W R ) -> ( Y e. _V /\ R e. _V ) )
12	10, 11	mpan 670	. . . . . . 7 |- ( Y W R -> ( Y e. _V /\ R e. _V ) )
13		op1stg 6675	. . . . . . 7 |- ( ( Y e. _V /\ R e. _V ) -> ( 1st ` <. Y , R >. ) = Y )
14	12, 13	syl 16	. . . . . 6 |- ( Y W R -> ( 1st ` <. Y , R >. ) = Y )
15	14	fveq2d 5779	. . . . 5 |- ( Y W R -> ( F ` ( 1st ` <. Y , R >. ) ) = ( F ` Y ) )
16	8, 15	syl5eq 2502	. . . 4 |- ( Y W R -> ( Y ( F o. 1st ) R ) = ( F ` Y ) )
17	16	eleq1d 2518	. . 3 |- ( Y W R -> ( ( Y ( F o. 1st ) R ) e. Y <-> ( F ` Y ) e. Y ) )
18	17	pm5.32i 637	. 2 |- ( ( Y W R /\ ( Y ( F o. 1st ) R ) e. Y ) <-> ( Y W R /\ ( F ` Y ) e. Y ) )
19		vex 3057	. . . . . . . . . 10 |- r e. _V
20		cnvexg 6610	. . . . . . . . . 10 |- ( r e. _V -> `' r e. _V )
21		imaexg 6601	. . . . . . . . . 10 |- ( `' r e. _V -> ( `' r " { y } ) e. _V )
22	19, 20, 21	mp2b 10	. . . . . . . . 9 |- ( `' r " { y } ) e. _V
23		vex 3057	. . . . . . . . . . . 12 |- u e. _V
24	19	inex1 4517	. . . . . . . . . . . 12 |- ( r i^i ( u X. u ) ) e. _V
25	23, 24	algrflem 6767	. . . . . . . . . . 11 |- ( u ( F o. 1st ) ( r i^i ( u X. u ) ) ) = ( F ` u )
26		fveq2 5775	. . . . . . . . . . 11 |- ( u = ( `' r " { y } ) -> ( F ` u ) = ( F ` ( `' r " { y } ) ) )
27	25, 26	syl5eq 2502	. . . . . . . . . 10 |- ( u = ( `' r " { y } ) -> ( u ( F o. 1st ) ( r i^i ( u X. u ) ) ) = ( F ` ( `' r " { y } ) ) )
28	27	eqeq1d 2452	. . . . . . . . 9 |- ( u = ( `' r " { y } ) -> ( ( u ( F o. 1st ) ( r i^i ( u X. u ) ) ) = y <-> ( F ` ( `' r " { y } ) ) = y ) )
29	22, 28	sbcie 3305	. . . . . . . 8 |- ( [. ( `' r " { y } ) / u ]. ( u ( F o. 1st ) ( r i^i ( u X. u ) ) ) = y <-> ( F ` ( `' r " { y } ) ) = y )
30	29	ralbii 2819	. . . . . . 7 |- ( A. y e. x [. ( `' r " { y } ) / u ]. ( u ( F o. 1st ) ( r i^i ( u X. u ) ) ) = y <-> A. y e. x ( F ` ( `' r " { y } ) ) = y )
31	30	anbi2i 694	. . . . . 6 |- ( ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u ( F o. 1st ) ( r i^i ( u X. u ) ) ) = y ) <-> ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) )
32	31	anbi2i 694	. . . . 5 |- ( ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u ( F o. 1st ) ( r i^i ( u X. u ) ) ) = y ) ) <-> ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) ) )
33	32	opabbii 4440	. . . 4 |- { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u ( F o. 1st ) ( r i^i ( u X. u ) ) ) = y ) ) } = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) ) }
34	9, 33	eqtr4i 2481	. . 3 |- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u ( F o. 1st ) ( r i^i ( u X. u ) ) ) = y ) ) }
35		fpwwe.2	. . 3 |- ( ph -> A e. _V )
36		vex 3057	. . . . 5 |- x e. _V
37	36, 19	algrflem 6767	. . . 4 |- ( x ( F o. 1st ) r ) = ( F ` x )
38		simp1 988	. . . . . . 7 |- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> x C_ A )
39		selpw 3951	. . . . . . 7 |- ( x e. ~P A <-> x C_ A )
40	38, 39	sylibr 212	. . . . . 6 |- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> x e. ~P A )
41		19.8a 1794	. . . . . . . 8 |- ( r We x -> E. r r We x )
42	41	3ad2ant3 1011	. . . . . . 7 |- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> E. r r We x )
43		ween 8292	. . . . . . 7 |- ( x e. dom card <-> E. r r We x )
44	42, 43	sylibr 212	. . . . . 6 |- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> x e. dom card )
45	40, 44	elind 3624	. . . . 5 |- ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> x e. ( ~P A i^i dom card ) )
46		fpwwe.3	. . . . 5 |- ( ( ph /\ x e. ( ~P A i^i dom card ) ) -> ( F ` x ) e. A )
47	45, 46	sylan2 474	. . . 4 |- ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( F ` x ) e. A )
48	37, 47	syl5eqel 2540	. . 3 |- ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x ( F o. 1st ) r ) e. A )
49		fpwwe.4	. . 3 |- X = U. dom W
50	34, 35, 48, 49	fpwwe2 8897	. 2 |- ( ph -> ( ( Y W R /\ ( Y ( F o. 1st ) R ) e. Y ) <-> ( Y = X /\ R = ( W ` X ) ) ) )
51	18, 50	syl5bbr 259	1 |- ( ph -> ( ( Y W R /\ ( F ` Y ) e. Y ) <-> ( Y = X /\ R = ( W ` X ) ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 965   = wceq 1370   E.wex 1587   e. wcel 1757   A.wral 2792   _Vcvv 3054   [.wsbc 3270   i^i cin 3411   C_ wss 3412   ~Pcpw 3944   {csn 3961   <.cop 3967   U.cuni 4175   class class class wbr 4376   {copab 4433   We wwe 4762   X. cxp 4922   `'ccnv 4923   dom cdm 4924   "cima 4927   o. ccom 4928   Rel wrel 4929   Fn wfn 5497   -onto->wfo 5500   ` cfv 5502  (class class class)co 6176   1stc1st 6661   cardccrd 8192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-rep 4487  ax-sep 4497  ax-nul 4505  ax-pow 4554  ax-pr 4615  ax-un 6458

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-reu 2799  df-rmo 2800  df-rab 2801  df-v 3056  df-sbc 3271  df-csb 3373  df-dif 3415  df-un 3417  df-in 3419  df-ss 3426  df-pss 3428  df-nul 3722  df-if 3876  df-pw 3946  df-sn 3962  df-pr 3964  df-tp 3966  df-op 3968  df-uni 4176  df-int 4213  df-iun 4257  df-br 4377  df-opab 4435  df-mpt 4436  df-tr 4470  df-eprel 4716  df-id 4720  df-po 4725  df-so 4726  df-fr 4763  df-se 4764  df-we 4765  df-ord 4806  df-on 4807  df-lim 4808  df-suc 4809  df-xp 4930  df-rel 4931  df-cnv 4932  df-co 4933  df-dm 4934  df-rn 4935  df-res 4936  df-ima 4937  df-iota 5465  df-fun 5504  df-fn 5505  df-f 5506  df-f1 5507  df-fo 5508  df-f1o 5509  df-fv 5510  df-isom 5511  df-riota 6137  df-ov 6179  df-1st 6663  df-recs 6918  df-en 7397  df-oi 7811  df-card 8196

This theorem is referenced by:  canth4  8901  canthnumlem  8902  canthp1lem2  8907