Metamath Proof Explorer

Theorem fodomacn

Description: A version of fodom that doesn't require the Axiom of Choice ax-ac . If A has choice sequences of length B , then any surjection from A to B can be inverted to an injection the other way. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion fodomacn 
|- ( A e. AC_ B -> ( F : A -onto-> B -> B ~<_ A ) )

Proof

Step Hyp Ref Expression
1 foelrn 
 |-  ( ( F : A -onto-> B /\ x e. B ) -> E. y e. A x = ( F ` y ) )
2 1 ralrimiva 
 |-  ( F : A -onto-> B -> A. x e. B E. y e. A x = ( F ` y ) )
3 fveq2 
 |-  ( y = ( f ` x ) -> ( F ` y ) = ( F ` ( f ` x ) ) )
4 3 eqeq2d 
 |-  ( y = ( f ` x ) -> ( x = ( F ` y ) <-> x = ( F ` ( f ` x ) ) ) )
5 4 acni3 
 |-  ( ( A e. AC_ B /\ A. x e. B E. y e. A x = ( F ` y ) ) -> E. f ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) )
6 2 5 sylan2 
 |-  ( ( A e. AC_ B /\ F : A -onto-> B ) -> E. f ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) )
7 simpll 
 |-  ( ( ( A e. AC_ B /\ F : A -onto-> B ) /\ ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) ) -> A e. AC_ B )
8 acnrcl 
 |-  ( A e. AC_ B -> B e. _V )
9 7 8 syl 
 |-  ( ( ( A e. AC_ B /\ F : A -onto-> B ) /\ ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) ) -> B e. _V )
10 simprl 
 |-  ( ( ( A e. AC_ B /\ F : A -onto-> B ) /\ ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) ) -> f : B --> A )
11 fveq2 
 |-  ( ( f ` y ) = ( f ` z ) -> ( F ` ( f ` y ) ) = ( F ` ( f ` z ) ) )
12 simprr 
 |-  ( ( ( A e. AC_ B /\ F : A -onto-> B ) /\ ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) ) -> A. x e. B x = ( F ` ( f ` x ) ) )
13 id 
 |-  ( x = y -> x = y )
14 2fveq3 
 |-  ( x = y -> ( F ` ( f ` x ) ) = ( F ` ( f ` y ) ) )
15 13 14 eqeq12d 
 |-  ( x = y -> ( x = ( F ` ( f ` x ) ) <-> y = ( F ` ( f ` y ) ) ) )
16 15 rspccva 
 |-  ( ( A. x e. B x = ( F ` ( f ` x ) ) /\ y e. B ) -> y = ( F ` ( f ` y ) ) )
17 id 
 |-  ( x = z -> x = z )
18 2fveq3 
 |-  ( x = z -> ( F ` ( f ` x ) ) = ( F ` ( f ` z ) ) )
19 17 18 eqeq12d 
 |-  ( x = z -> ( x = ( F ` ( f ` x ) ) <-> z = ( F ` ( f ` z ) ) ) )
20 19 rspccva 
 |-  ( ( A. x e. B x = ( F ` ( f ` x ) ) /\ z e. B ) -> z = ( F ` ( f ` z ) ) )
21 16 20 eqeqan12d 
 |-  ( ( ( A. x e. B x = ( F ` ( f ` x ) ) /\ y e. B ) /\ ( A. x e. B x = ( F ` ( f ` x ) ) /\ z e. B ) ) -> ( y = z <-> ( F ` ( f ` y ) ) = ( F ` ( f ` z ) ) ) )
22 21 anandis 
 |-  ( ( A. x e. B x = ( F ` ( f ` x ) ) /\ ( y e. B /\ z e. B ) ) -> ( y = z <-> ( F ` ( f ` y ) ) = ( F ` ( f ` z ) ) ) )
23 12 22 sylan 
 |-  ( ( ( ( A e. AC_ B /\ F : A -onto-> B ) /\ ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) ) /\ ( y e. B /\ z e. B ) ) -> ( y = z <-> ( F ` ( f ` y ) ) = ( F ` ( f ` z ) ) ) )
24 11 23 imbitrrid 
 |-  ( ( ( ( A e. AC_ B /\ F : A -onto-> B ) /\ ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) ) /\ ( y e. B /\ z e. B ) ) -> ( ( f ` y ) = ( f ` z ) -> y = z ) )
25 24 ralrimivva 
 |-  ( ( ( A e. AC_ B /\ F : A -onto-> B ) /\ ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) ) -> A. y e. B A. z e. B ( ( f ` y ) = ( f ` z ) -> y = z ) )
26 dff13 
 |-  ( f : B -1-1-> A <-> ( f : B --> A /\ A. y e. B A. z e. B ( ( f ` y ) = ( f ` z ) -> y = z ) ) )
27 10 25 26 sylanbrc 
 |-  ( ( ( A e. AC_ B /\ F : A -onto-> B ) /\ ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) ) -> f : B -1-1-> A )
28 f1dom2g 
 |-  ( ( B e. _V /\ A e. AC_ B /\ f : B -1-1-> A ) -> B ~<_ A )
29 9 7 27 28 syl3anc 
 |-  ( ( ( A e. AC_ B /\ F : A -onto-> B ) /\ ( f : B --> A /\ A. x e. B x = ( F ` ( f ` x ) ) ) ) -> B ~<_ A )
30 6 29 exlimddv 
 |-  ( ( A e. AC_ B /\ F : A -onto-> B ) -> B ~<_ A )
31 30 ex 
 |-  ( A e. AC_ B -> ( F : A -onto-> B -> B ~<_ A ) )