Metamath Proof Explorer

Theorem cff1

Description: There is always a map from ( cfA ) to A (this is a stronger condition than the definition, which only presupposes a map from some y ~( cfA ) . (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Assertion cff1 
|- ( A e. On -> E. f ( f : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) )

Proof

Step Hyp Ref Expression
1 cfval 
 |-  ( A e. On -> ( cf ` A ) = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } )
2 cardon 
 |-  ( card ` y ) e. On
3 eleq1 
 |-  ( x = ( card ` y ) -> ( x e. On <-> ( card ` y ) e. On ) )
4 2 3 mpbiri 
 |-  ( x = ( card ` y ) -> x e. On )
5 4 adantr 
 |-  ( ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) -> x e. On )
6 5 exlimiv 
 |-  ( E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) -> x e. On )
7 6 abssi 
 |-  { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } C_ On
8 cflem 
 |-  ( A e. On -> E. x E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) )
9 abn0 
 |-  ( { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } =/= (/) <-> E. x E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) )
10 8 9 sylibr 
 |-  ( A e. On -> { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } =/= (/) )
11 onint 
 |-  ( ( { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } C_ On /\ { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } =/= (/) ) -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } )
12 7 10 11 sylancr 
 |-  ( A e. On -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } )
13 1 12 eqeltrd 
 |-  ( A e. On -> ( cf ` A ) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } )
14 fvex 
 |-  ( cf ` A ) e. _V
15 eqeq1 
 |-  ( x = ( cf ` A ) -> ( x = ( card ` y ) <-> ( cf ` A ) = ( card ` y ) ) )
16 15 anbi1d 
 |-  ( x = ( cf ` A ) -> ( ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) <-> ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) ) )
17 16 exbidv 
 |-  ( x = ( cf ` A ) -> ( E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) <-> E. y ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) ) )
18 14 17 elab 
 |-  ( ( cf ` A ) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) } <-> E. y ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) )
19 13 18 sylib 
 |-  ( A e. On -> E. y ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) )
20 simplr 
 |-  ( ( ( A e. On /\ ( cf ` A ) = ( card ` y ) ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) -> ( cf ` A ) = ( card ` y ) )
21 onss 
 |-  ( A e. On -> A C_ On )
22 sstr 
 |-  ( ( y C_ A /\ A C_ On ) -> y C_ On )
23 21 22 sylan2 
 |-  ( ( y C_ A /\ A e. On ) -> y C_ On )
24 23 ancoms 
 |-  ( ( A e. On /\ y C_ A ) -> y C_ On )
25 24 ad2ant2r 
 |-  ( ( ( A e. On /\ ( cf ` A ) = ( card ` y ) ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) -> y C_ On )
26 vex 
 |-  y e. _V
27 onssnum 
 |-  ( ( y e. _V /\ y C_ On ) -> y e. dom card )
28 26 27 mpan 
 |-  ( y C_ On -> y e. dom card )
29 cardid2 
 |-  ( y e. dom card -> ( card ` y ) ~~ y )
30 28 29 syl 
 |-  ( y C_ On -> ( card ` y ) ~~ y )
31 30 adantl 
 |-  ( ( ( cf ` A ) = ( card ` y ) /\ y C_ On ) -> ( card ` y ) ~~ y )
32 breq1 
 |-  ( ( cf ` A ) = ( card ` y ) -> ( ( cf ` A ) ~~ y <-> ( card ` y ) ~~ y ) )
33 32 adantr 
 |-  ( ( ( cf ` A ) = ( card ` y ) /\ y C_ On ) -> ( ( cf ` A ) ~~ y <-> ( card ` y ) ~~ y ) )
34 31 33 mpbird 
 |-  ( ( ( cf ` A ) = ( card ` y ) /\ y C_ On ) -> ( cf ` A ) ~~ y )
35 bren 
 |-  ( ( cf ` A ) ~~ y <-> E. f f : ( cf ` A ) -1-1-onto-> y )
36 34 35 sylib 
 |-  ( ( ( cf ` A ) = ( card ` y ) /\ y C_ On ) -> E. f f : ( cf ` A ) -1-1-onto-> y )
37 20 25 36 syl2anc 
 |-  ( ( ( A e. On /\ ( cf ` A ) = ( card ` y ) ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) -> E. f f : ( cf ` A ) -1-1-onto-> y )
38 f1of1 
 |-  ( f : ( cf ` A ) -1-1-onto-> y -> f : ( cf ` A ) -1-1-> y )
39 f1ss 
 |-  ( ( f : ( cf ` A ) -1-1-> y /\ y C_ A ) -> f : ( cf ` A ) -1-1-> A )
40 39 ancoms 
 |-  ( ( y C_ A /\ f : ( cf ` A ) -1-1-> y ) -> f : ( cf ` A ) -1-1-> A )
41 38 40 sylan2 
 |-  ( ( y C_ A /\ f : ( cf ` A ) -1-1-onto-> y ) -> f : ( cf ` A ) -1-1-> A )
42 41 adantlr 
 |-  ( ( ( y C_ A /\ A. z e. A E. s e. y z C_ s ) /\ f : ( cf ` A ) -1-1-onto-> y ) -> f : ( cf ` A ) -1-1-> A )
43 42 3adant1 
 |-  ( ( ( A e. On /\ ( cf ` A ) = ( card ` y ) ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) /\ f : ( cf ` A ) -1-1-onto-> y ) -> f : ( cf ` A ) -1-1-> A )
44 f1ofo 
 |-  ( f : ( cf ` A ) -1-1-onto-> y -> f : ( cf ` A ) -onto-> y )
45 foelrn 
 |-  ( ( f : ( cf ` A ) -onto-> y /\ s e. y ) -> E. w e. ( cf ` A ) s = ( f ` w ) )
46 sseq2 
 |-  ( s = ( f ` w ) -> ( z C_ s <-> z C_ ( f ` w ) ) )
47 46 biimpcd 
 |-  ( z C_ s -> ( s = ( f ` w ) -> z C_ ( f ` w ) ) )
48 47 reximdv 
 |-  ( z C_ s -> ( E. w e. ( cf ` A ) s = ( f ` w ) -> E. w e. ( cf ` A ) z C_ ( f ` w ) ) )
49 45 48 syl5com 
 |-  ( ( f : ( cf ` A ) -onto-> y /\ s e. y ) -> ( z C_ s -> E. w e. ( cf ` A ) z C_ ( f ` w ) ) )
50 49 rexlimdva 
 |-  ( f : ( cf ` A ) -onto-> y -> ( E. s e. y z C_ s -> E. w e. ( cf ` A ) z C_ ( f ` w ) ) )
51 50 ralimdv 
 |-  ( f : ( cf ` A ) -onto-> y -> ( A. z e. A E. s e. y z C_ s -> A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) )
52 44 51 syl 
 |-  ( f : ( cf ` A ) -1-1-onto-> y -> ( A. z e. A E. s e. y z C_ s -> A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) )
53 52 impcom 
 |-  ( ( A. z e. A E. s e. y z C_ s /\ f : ( cf ` A ) -1-1-onto-> y ) -> A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) )
54 53 adantll 
 |-  ( ( ( y C_ A /\ A. z e. A E. s e. y z C_ s ) /\ f : ( cf ` A ) -1-1-onto-> y ) -> A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) )
55 54 3adant1 
 |-  ( ( ( A e. On /\ ( cf ` A ) = ( card ` y ) ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) /\ f : ( cf ` A ) -1-1-onto-> y ) -> A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) )
56 43 55 jca 
 |-  ( ( ( A e. On /\ ( cf ` A ) = ( card ` y ) ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) /\ f : ( cf ` A ) -1-1-onto-> y ) -> ( f : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) )
57 56 3expia 
 |-  ( ( ( A e. On /\ ( cf ` A ) = ( card ` y ) ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) -> ( f : ( cf ` A ) -1-1-onto-> y -> ( f : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) ) )
58 57 eximdv 
 |-  ( ( ( A e. On /\ ( cf ` A ) = ( card ` y ) ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) -> ( E. f f : ( cf ` A ) -1-1-onto-> y -> E. f ( f : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) ) )
59 37 58 mpd 
 |-  ( ( ( A e. On /\ ( cf ` A ) = ( card ` y ) ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) -> E. f ( f : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) )
60 59 expl 
 |-  ( A e. On -> ( ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) -> E. f ( f : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) ) )
61 60 exlimdv 
 |-  ( A e. On -> ( E. y ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A. z e. A E. s e. y z C_ s ) ) -> E. f ( f : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) ) )
62 19 61 mpd 
 |-  ( A e. On -> E. f ( f : ( cf ` A ) -1-1-> A /\ A. z e. A E. w e. ( cf ` A ) z C_ ( f ` w ) ) )