Theorem f1mo

Description: A function that maps a set with at most one element to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024)

	Ref	Expression
Assertion	f1mo	⊢ ( ( ∃* 𝑥 𝑥 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐹 : 𝐴 –1-1→ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mo0sn	⊢ ( ∃* 𝑥 𝑥 ∈ 𝐴 ↔ ( 𝐴 = ∅ ∨ ∃ 𝑦 𝐴 = { 𝑦 } ) )
2		f102g	⊢ ( ( 𝐴 = ∅ ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐹 : 𝐴 –1-1→ 𝐵 )
3		vex	⊢ 𝑦 ∈ V
4		f1sn2g	⊢ ( ( 𝑦 ∈ V ∧ 𝐹 : { 𝑦 } ⟶ 𝐵 ) → 𝐹 : { 𝑦 } –1-1→ 𝐵 )
5	3 4	mpan	⊢ ( 𝐹 : { 𝑦 } ⟶ 𝐵 → 𝐹 : { 𝑦 } –1-1→ 𝐵 )
6		feq2	⊢ ( 𝐴 = { 𝑦 } → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : { 𝑦 } ⟶ 𝐵 ) )
7		f1eq2	⊢ ( 𝐴 = { 𝑦 } → ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ 𝐹 : { 𝑦 } –1-1→ 𝐵 ) )
8	6 7	imbi12d	⊢ ( 𝐴 = { 𝑦 } → ( ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 : 𝐴 –1-1→ 𝐵 ) ↔ ( 𝐹 : { 𝑦 } ⟶ 𝐵 → 𝐹 : { 𝑦 } –1-1→ 𝐵 ) ) )
9	5 8	mpbiri	⊢ ( 𝐴 = { 𝑦 } → ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 : 𝐴 –1-1→ 𝐵 ) )
10	9	exlimiv	⊢ ( ∃ 𝑦 𝐴 = { 𝑦 } → ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 : 𝐴 –1-1→ 𝐵 ) )
11	10	imp	⊢ ( ( ∃ 𝑦 𝐴 = { 𝑦 } ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐹 : 𝐴 –1-1→ 𝐵 )
12	2 11	jaoian	⊢ ( ( ( 𝐴 = ∅ ∨ ∃ 𝑦 𝐴 = { 𝑦 } ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐹 : 𝐴 –1-1→ 𝐵 )
13	1 12	sylanb	⊢ ( ( ∃* 𝑥 𝑥 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐹 : 𝐴 –1-1→ 𝐵 )