Metamath Proof Explorer

Theorem fpwwe

Description: Given any function F from the powerset of A to A , canth2 gives that the function is not injective, but we can say rather more than that. There is a unique well-ordered subset <. X , ( WX ) >. 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 . Theorem 1.1 of KanamoriPincus p. 415. (Contributed by Mario Carneiro, 18-May-2015) (Revised by AV, 20-Jul-2024)

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

Proof

Step Hyp Ref Expression
1 fpwwe.1 
 |-  W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) ) }
2 fpwwe.2 
 |-  ( ph -> A e. V )
3 fpwwe.3 
 |-  ( ( ph /\ x e. ( ~P A i^i dom card ) ) -> ( F ` x ) e. A )
4 fpwwe.4 
 |-  X = U. dom W
5 df-ov 
 |-  ( Y ( F o. 1st ) R ) = ( ( F o. 1st ) ` <. Y , R >. )
6 fo1st 
 |-  1st : _V -onto-> _V
7 fofn 
 |-  ( 1st : _V -onto-> _V -> 1st Fn _V )
8 6 7 ax-mp 
 |-  1st Fn _V
9 opex 
 |-  <. Y , R >. e. _V
10 fvco2 
 |-  ( ( 1st Fn _V /\ <. Y , R >. e. _V ) -> ( ( F o. 1st ) ` <. Y , R >. ) = ( F ` ( 1st ` <. Y , R >. ) ) )
11 8 9 10 mp2an 
 |-  ( ( F o. 1st ) ` <. Y , R >. ) = ( F ` ( 1st ` <. Y , R >. ) )
12 5 11 eqtri 
 |-  ( Y ( F o. 1st ) R ) = ( F ` ( 1st ` <. Y , R >. ) )
13 1 bropaex12 
 |-  ( Y W R -> ( Y e. _V /\ R e. _V ) )
14 op1stg 
 |-  ( ( Y e. _V /\ R e. _V ) -> ( 1st ` <. Y , R >. ) = Y )
15 13 14 syl 
 |-  ( Y W R -> ( 1st ` <. Y , R >. ) = Y )
16 15 fveq2d 
 |-  ( Y W R -> ( F ` ( 1st ` <. Y , R >. ) ) = ( F ` Y ) )
17 12 16 eqtrid 
 |-  ( Y W R -> ( Y ( F o. 1st ) R ) = ( F ` Y ) )
18 17 eleq1d 
 |-  ( Y W R -> ( ( Y ( F o. 1st ) R ) e. Y <-> ( F ` Y ) e. Y ) )
19 18 pm5.32i 
 |-  ( ( Y W R /\ ( Y ( F o. 1st ) R ) e. Y ) <-> ( Y W R /\ ( F ` Y ) e. Y ) )
20 vex 
 |-  r e. _V
21 20 cnvex 
 |-  `' r e. _V
22 21 imaex 
 |-  ( `' r " { y } ) e. _V
23 vex 
 |-  u e. _V
24 20 inex1 
 |-  ( r i^i ( u X. u ) ) e. _V
25 23 24 opco1i 
 |-  ( u ( F o. 1st ) ( r i^i ( u X. u ) ) ) = ( F ` u )
26 fveq2 
 |-  ( u = ( `' r " { y } ) -> ( F ` u ) = ( F ` ( `' r " { y } ) ) )
27 25 26 eqtrid 
 |-  ( u = ( `' r " { y } ) -> ( u ( F o. 1st ) ( r i^i ( u X. u ) ) ) = ( F ` ( `' r " { y } ) ) )
28 27 eqeq1d 
 |-  ( u = ( `' r " { y } ) -> ( ( u ( F o. 1st ) ( r i^i ( u X. u ) ) ) = y <-> ( F ` ( `' r " { y } ) ) = y ) )
29 22 28 sbcie 
 |-  ( [. ( `' r " { y } ) / u ]. ( u ( F o. 1st ) ( r i^i ( u X. u ) ) ) = y <-> ( F ` ( `' r " { y } ) ) = y )
30 29 ralbii 
 |-  ( 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 
 |-  ( ( 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 
 |-  ( ( ( 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 
 |-  { <. 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 1 33 eqtr4i 
 |-  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 vex 
 |-  x e. _V
36 35 20 opco1i 
 |-  ( x ( F o. 1st ) r ) = ( F ` x )
37 simp1 
 |-  ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> x C_ A )
38 velpw 
 |-  ( x e. ~P A <-> x C_ A )
39 37 38 sylibr 
 |-  ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> x e. ~P A )
40 19.8a 
 |-  ( r We x -> E. r r We x )
41 40 3ad2ant3 
 |-  ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> E. r r We x )
42 ween 
 |-  ( x e. dom card <-> E. r r We x )
43 41 42 sylibr 
 |-  ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> x e. dom card )
44 39 43 elind 
 |-  ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> x e. ( ~P A i^i dom card ) )
45 44 3 sylan2 
 |-  ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( F ` x ) e. A )
46 36 45 eqeltrid 
 |-  ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x ( F o. 1st ) r ) e. A )
47 34 2 46 4 fpwwe2 
 |-  ( ph -> ( ( Y W R /\ ( Y ( F o. 1st ) R ) e. Y ) <-> ( Y = X /\ R = ( W ` X ) ) ) )
48 19 47 bitr3id 
 |-  ( ph -> ( ( Y W R /\ ( F ` Y ) e. Y ) <-> ( Y = X /\ R = ( W ` X ) ) ) )