This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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→ 𝐵 )