Theorem f1dom4g

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 nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024)

	Ref	Expression
Assertion	f1dom4g	|- ( ( ( F e. V /\ A e. W /\ B e. X ) /\ 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	3ad2antl1	|- ( ( ( F e. V /\ A e. W /\ B e. X ) /\ F : A -1-1-> B ) -> E. f f : A -1-1-> B )
5		brdom2g	|- ( ( A e. W /\ B e. X ) -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
6	5	3adant1	|- ( ( F e. V /\ A e. W /\ B e. X ) -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
7	6	adantr	|- ( ( ( F e. V /\ A e. W /\ B e. X ) /\ F : A -1-1-> B ) -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
8	4 7	mpbird	|- ( ( ( F e. V /\ A e. W /\ B e. X ) /\ F : A -1-1-> B ) -> A ~<_ B )