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		f1oeq1	⊢ ( { ⟨ 𝑎 , 𝑏 ⟩ } = { ⟨ 𝐴 , 𝑏 ⟩ } → ( { ⟨ 𝑎 , 𝑏 ⟩ } : { 𝐴 } –1-1-onto→ { 𝑏 } ↔ { ⟨ 𝐴 , 𝑏 ⟩ } : { 𝐴 } –1-1-onto→ { 𝑏 } ) )
6	4 5	syl	⊢ ( 𝑎 = 𝐴 → ( { ⟨ 𝑎 , 𝑏 ⟩ } : { 𝐴 } –1-1-onto→ { 𝑏 } ↔ { ⟨ 𝐴 , 𝑏 ⟩ } : { 𝐴 } –1-1-onto→ { 𝑏 } ) )
7	2 6	bitrd	⊢ ( 𝑎 = 𝐴 → ( { ⟨ 𝑎 , 𝑏 ⟩ } : { 𝑎 } –1-1-onto→ { 𝑏 } ↔ { ⟨ 𝐴 , 𝑏 ⟩ } : { 𝐴 } –1-1-onto→ { 𝑏 } ) )
8		sneq	⊢ ( 𝑏 = 𝐵 → { 𝑏 } = { 𝐵 } )
9	8	f1oeq3d	⊢ ( 𝑏 = 𝐵 → ( { ⟨ 𝐴 , 𝑏 ⟩ } : { 𝐴 } –1-1-onto→ { 𝑏 } ↔ { ⟨ 𝐴 , 𝑏 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } ) )
10		opeq2	⊢ ( 𝑏 = 𝐵 → ⟨ 𝐴 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
11	10	sneqd	⊢ ( 𝑏 = 𝐵 → { ⟨ 𝐴 , 𝑏 ⟩ } = { ⟨ 𝐴 , 𝐵 ⟩ } )
12		f1oeq1	⊢ ( { ⟨ 𝐴 , 𝑏 ⟩ } = { ⟨ 𝐴 , 𝐵 ⟩ } → ( { ⟨ 𝐴 , 𝑏 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } ↔ { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } ) )
13	11 12	syl	⊢ ( 𝑏 = 𝐵 → ( { ⟨ 𝐴 , 𝑏 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } ↔ { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } ) )
14	9 13	bitrd	⊢ ( 𝑏 = 𝐵 → ( { ⟨ 𝐴 , 𝑏 ⟩ } : { 𝐴 } –1-1-onto→ { 𝑏 } ↔ { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } ) )
15		vex	⊢ 𝑎 ∈ V
16		vex	⊢ 𝑏 ∈ V
17	15 16	f1osn	⊢ { ⟨ 𝑎 , 𝑏 ⟩ } : { 𝑎 } –1-1-onto→ { 𝑏 }
18	7 14 17	vtocl2g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } )