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

Metamath Proof Explorer

Theorem f1sng

Description: A singleton of an ordered pair is a one-to-one function. (Contributed by AV, 17-Apr-2021)

Ref Expression
Assertion f1sng ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1→ 𝑊 )

Proof

Step Hyp Ref Expression
1 f1osng ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } )
2 f1of1 ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } → { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1→ { 𝐵 } )
3 1 2 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1→ { 𝐵 } )
4 snssi ⊢ ( 𝐵 ∈ 𝑊 → { 𝐵 } ⊆ 𝑊 )
5 4 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { 𝐵 } ⊆ 𝑊 )
6 f1ss ⊢ ( ( { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1→ { 𝐵 } ∧ { 𝐵 } ⊆ 𝑊 ) → { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1→ 𝑊 )
7 3 5 6 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1→ 𝑊 )