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	$$⊢\left(\left(F\in V\wedge A\in W\wedge B\in X\right)\wedge F:A\underset{1-1}{⟶}B\right)\to A\preccurlyeq B$$

Proof

Step	Hyp	Ref	Expression
1		f1eq1	$$⊢f=F\to \left(f:A\underset{1-1}{⟶}B\leftrightarrow F:A\underset{1-1}{⟶}B\right)$$
2	1	spcegv	$$⊢F\in V\to \left(F:A\underset{1-1}{⟶}B\to \exists ff:A\underset{1-1}{⟶}B\right)$$
3	2	imp	$$⊢\left(F\in V\wedge F:A\underset{1-1}{⟶}B\right)\to \exists ff:A\underset{1-1}{⟶}B$$
4	3	3ad2antl1	$$⊢\left(\left(F\in V\wedge A\in W\wedge B\in X\right)\wedge F:A\underset{1-1}{⟶}B\right)\to \exists ff:A\underset{1-1}{⟶}B$$
5		brdom2g	$$⊢\left(A\in W\wedge B\in X\right)\to \left(A\preccurlyeq B\leftrightarrow \exists ff:A\underset{1-1}{⟶}B\right)$$
6	5	3adant1	$$⊢\left(F\in V\wedge A\in W\wedge B\in X\right)\to \left(A\preccurlyeq B\leftrightarrow \exists ff:A\underset{1-1}{⟶}B\right)$$
7	6	adantr	$$⊢\left(\left(F\in V\wedge A\in W\wedge B\in X\right)\wedge F:A\underset{1-1}{⟶}B\right)\to \left(A\preccurlyeq B\leftrightarrow \exists ff:A\underset{1-1}{⟶}B\right)$$
8	4 7	mpbird	$$⊢\left(\left(F\in V\wedge A\in W\wedge B\in X\right)\wedge F:A\underset{1-1}{⟶}B\right)\to A\preccurlyeq B$$