This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem f1oen2g

Description: The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 10-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 f1of 
 |-  ( F : A -1-1-onto-> B -> F : A --> B )
2 fex2 
 |-  ( ( F : A --> B /\ A e. V /\ B e. W ) -> F e. _V )
3 1 2 syl3an1 
 |-  ( ( F : A -1-1-onto-> B /\ A e. V /\ B e. W ) -> F e. _V )
4 3 3coml 
 |-  ( ( A e. V /\ B e. W /\ F : A -1-1-onto-> B ) -> F e. _V )
5 simp3 
 |-  ( ( A e. V /\ B e. W /\ F : A -1-1-onto-> B ) -> F : A -1-1-onto-> B )
6 f1oen3g 
 |-  ( ( F e. _V /\ F : A -1-1-onto-> B ) -> A ~~ B )
7 4 5 6 syl2anc 
 |-  ( ( A e. V /\ B e. W /\ F : A -1-1-onto-> B ) -> A ~~ B )