Theorem f102g

Description: A function that maps the empty set to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024)

	Ref	Expression
Assertion	f102g	$$⊢\left(A=\varnothing \wedge F:A⟶B\right)\to F:A\underset{1-1}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		feq2	$$⊢A=\varnothing \to \left(F:A⟶B\leftrightarrow F:\varnothing ⟶B\right)$$
2	1	biimpa	$$⊢\left(A=\varnothing \wedge F:A⟶B\right)\to F:\varnothing ⟶B$$
3		f0bi	$$⊢F:\varnothing ⟶B\leftrightarrow F=\varnothing$$
4		f10	$$⊢\varnothing :\varnothing \underset{1-1}{⟶}B$$
5		f1eq1	$$⊢F=\varnothing \to \left(F:\varnothing \underset{1-1}{⟶}B\leftrightarrow \varnothing :\varnothing \underset{1-1}{⟶}B\right)$$
6	4 5	mpbiri	$$⊢F=\varnothing \to F:\varnothing \underset{1-1}{⟶}B$$
7	3 6	sylbi	$$⊢F:\varnothing ⟶B\to F:\varnothing \underset{1-1}{⟶}B$$
8	2 7	syl	$$⊢\left(A=\varnothing \wedge F:A⟶B\right)\to F:\varnothing \underset{1-1}{⟶}B$$
9		f1eq2	$$⊢A=\varnothing \to \left(F:A\underset{1-1}{⟶}B\leftrightarrow F:\varnothing \underset{1-1}{⟶}B\right)$$
10	9	adantr	$$⊢\left(A=\varnothing \wedge F:A⟶B\right)\to \left(F:A\underset{1-1}{⟶}B\leftrightarrow F:\varnothing \underset{1-1}{⟶}B\right)$$
11	8 10	mpbird	$$⊢\left(A=\varnothing \wedge F:A⟶B\right)\to F:A\underset{1-1}{⟶}B$$