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

Metamath Proof Explorer

Theorem f1dom3g

Description: The domain of a one-to-one set function is dominated by its codomain when the latter is a set. This variation of f1domg does not require the Axiom of Replacement nor the Axiom of Power Sets. (Contributed by BTernaryTau, 9-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 f1eq1 
 |-  ( f = F -> ( f : A -1-1-> B <-> F : A -1-1-> B ) )
2 1 spcegv 
 |-  ( F e. V -> ( F : A -1-1-> B -> E. f f : A -1-1-> B ) )
3 2 imp 
 |-  ( ( F e. V /\ F : A -1-1-> B ) -> E. f f : A -1-1-> B )
4 3 3adant2 
 |-  ( ( F e. V /\ B e. W /\ F : A -1-1-> B ) -> E. f f : A -1-1-> B )
5 brdomg 
 |-  ( B e. W -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
6 5 3ad2ant2 
 |-  ( ( F e. V /\ B e. W /\ F : A -1-1-> B ) -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
7 4 6 mpbird 
 |-  ( ( F e. V /\ B e. W /\ F : A -1-1-> B ) -> A ~<_ B )