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

Metamath Proof Explorer

Theorem f1sn2g

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

Ref Expression
Assertion f1sn2g ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : { 𝐴 } ⟶ 𝐵 ) → 𝐹 : { 𝐴 } –1-1→ 𝐵 )

Proof

Step Hyp Ref Expression
1 fsn2g ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 : { 𝐴 } ⟶ 𝐵 ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) ) )
2 1 biimpa ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : { 𝐴 } ⟶ 𝐵 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) )
3 2 simpld ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : { 𝐴 } ⟶ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 )
4 f1sng ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } : { 𝐴 } –1-1→ 𝐵 )
5 3 4 syldan ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : { 𝐴 } ⟶ 𝐵 ) → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } : { 𝐴 } –1-1→ 𝐵 )
6 f1eq1 ⊢ ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } → ( 𝐹 : { 𝐴 } –1-1→ 𝐵 ↔ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } : { 𝐴 } –1-1→ 𝐵 ) )
7 2 6 simpl2im ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : { 𝐴 } ⟶ 𝐵 ) → ( 𝐹 : { 𝐴 } –1-1→ 𝐵 ↔ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } : { 𝐴 } –1-1→ 𝐵 ) )
8 5 7 mpbird ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : { 𝐴 } ⟶ 𝐵 ) → 𝐹 : { 𝐴 } –1-1→ 𝐵 )