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	⊢ ( ( 𝐴 = ∅ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐹 : 𝐴 –1-1→ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		feq2	⊢ ( 𝐴 = ∅ → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : ∅ ⟶ 𝐵 ) )
2	1	biimpa	⊢ ( ( 𝐴 = ∅ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐹 : ∅ ⟶ 𝐵 )
3		f0bi	⊢ ( 𝐹 : ∅ ⟶ 𝐵 ↔ 𝐹 = ∅ )
4		f10	⊢ ∅ : ∅ –1-1→ 𝐵
5		f1eq1	⊢ ( 𝐹 = ∅ → ( 𝐹 : ∅ –1-1→ 𝐵 ↔ ∅ : ∅ –1-1→ 𝐵 ) )
6	4 5	mpbiri	⊢ ( 𝐹 = ∅ → 𝐹 : ∅ –1-1→ 𝐵 )
7	3 6	sylbi	⊢ ( 𝐹 : ∅ ⟶ 𝐵 → 𝐹 : ∅ –1-1→ 𝐵 )
8	2 7	syl	⊢ ( ( 𝐴 = ∅ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐹 : ∅ –1-1→ 𝐵 )
9		f1eq2	⊢ ( 𝐴 = ∅ → ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ 𝐹 : ∅ –1-1→ 𝐵 ) )
10	9	adantr	⊢ ( ( 𝐴 = ∅ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ 𝐹 : ∅ –1-1→ 𝐵 ) )
11	8 10	mpbird	⊢ ( ( 𝐴 = ∅ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐹 : 𝐴 –1-1→ 𝐵 )