Metamath Proof Explorer

Theorem f1oen4g

Description: The domain and range of a one-to-one, onto set function are equinumerous. This variation of f1oeng does not require the Axiom of Replacement nor the Axiom of Power Sets nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024)

Ref Expression
Assertion f1oen4g 
|- ( ( ( F e. V /\ A e. W /\ B e. X ) /\ F : A -1-1-onto-> B ) -> A ~~ B )

Proof

Step Hyp Ref Expression
1 f1oeq1 
 |-  ( f = F -> ( f : A -1-1-onto-> B <-> F : A -1-1-onto-> B ) )
2 1 spcegv 
 |-  ( F e. V -> ( F : A -1-1-onto-> B -> E. f f : A -1-1-onto-> B ) )
3 2 imp 
 |-  ( ( F e. V /\ F : A -1-1-onto-> B ) -> E. f f : A -1-1-onto-> B )
4 3 3ad2antl1 
 |-  ( ( ( F e. V /\ A e. W /\ B e. X ) /\ F : A -1-1-onto-> B ) -> E. f f : A -1-1-onto-> B )
5 breng 
 |-  ( ( A e. W /\ B e. X ) -> ( A ~~ B <-> E. f f : A -1-1-onto-> B ) )
6 5 3adant1 
 |-  ( ( F e. V /\ A e. W /\ B e. X ) -> ( A ~~ B <-> E. f f : A -1-1-onto-> B ) )
7 6 adantr 
 |-  ( ( ( F e. V /\ A e. W /\ B e. X ) /\ F : A -1-1-onto-> B ) -> ( A ~~ B <-> E. f f : A -1-1-onto-> B ) )
8 4 7 mpbird 
 |-  ( ( ( F e. V /\ A e. W /\ B e. X ) /\ F : A -1-1-onto-> B ) -> A ~~ B )