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

Metamath Proof Explorer

Theorem f1osng

Description: A singleton of an ordered pair is one-to-one onto function. (Contributed by Mario Carneiro, 12-Jan-2013)

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

Proof

Step Hyp Ref Expression
1 sneq ⊢ ( 𝑎 = 𝐴 → { 𝑎 } = { 𝐴 } )
2 1 f1oeq2d ⊢ ( 𝑎 = 𝐴 → ( { ⟨ 𝑎 , 𝑏 ⟩ } : { 𝑎 } –1-1-onto→ { 𝑏 } ↔ { ⟨ 𝑎 , 𝑏 ⟩ } : { 𝐴 } –1-1-onto→ { 𝑏 } ) )
3 opeq1 ⊢ ( 𝑎 = 𝐴 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝑏 ⟩ )
4 3 sneqd ⊢ ( 𝑎 = 𝐴 → { ⟨ 𝑎 , 𝑏 ⟩ } = { ⟨ 𝐴 , 𝑏 ⟩ } )
5 4 f1oeq1d ⊢ ( 𝑎 = 𝐴 → ( { ⟨ 𝑎 , 𝑏 ⟩ } : { 𝐴 } –1-1-onto→ { 𝑏 } ↔ { ⟨ 𝐴 , 𝑏 ⟩ } : { 𝐴 } –1-1-onto→ { 𝑏 } ) )
6 2 5 bitrd ⊢ ( 𝑎 = 𝐴 → ( { ⟨ 𝑎 , 𝑏 ⟩ } : { 𝑎 } –1-1-onto→ { 𝑏 } ↔ { ⟨ 𝐴 , 𝑏 ⟩ } : { 𝐴 } –1-1-onto→ { 𝑏 } ) )
7 sneq ⊢ ( 𝑏 = 𝐵 → { 𝑏 } = { 𝐵 } )
8 7 f1oeq3d ⊢ ( 𝑏 = 𝐵 → ( { ⟨ 𝐴 , 𝑏 ⟩ } : { 𝐴 } –1-1-onto→ { 𝑏 } ↔ { ⟨ 𝐴 , 𝑏 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } ) )
9 opeq2 ⊢ ( 𝑏 = 𝐵 → ⟨ 𝐴 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
10 9 sneqd ⊢ ( 𝑏 = 𝐵 → { ⟨ 𝐴 , 𝑏 ⟩ } = { ⟨ 𝐴 , 𝐵 ⟩ } )
11 10 f1oeq1d ⊢ ( 𝑏 = 𝐵 → ( { ⟨ 𝐴 , 𝑏 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } ↔ { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } ) )
12 8 11 bitrd ⊢ ( 𝑏 = 𝐵 → ( { ⟨ 𝐴 , 𝑏 ⟩ } : { 𝐴 } –1-1-onto→ { 𝑏 } ↔ { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } ) )
13 vex ⊢ 𝑎 ∈ V
14 vex ⊢ 𝑏 ∈ V
15 13 14 f1osn ⊢ { ⟨ 𝑎 , 𝑏 ⟩ } : { 𝑎 } –1-1-onto→ { 𝑏 }
16 6 12 15 vtocl2g ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } )