Theorem f1osn

Description: A singleton of an ordered pair is one-to-one onto function. (Contributed by NM, 18-May-1998) (Proof shortened by Andrew Salmon, 22-Oct-2011)

	Ref	Expression
Hypotheses	f1osn.1	⊢ 𝐴 ∈ V
	f1osn.2	⊢ 𝐵 ∈ V
Assertion	f1osn	⊢ { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 }

Proof

Step	Hyp	Ref	Expression
1		f1osn.1	⊢ 𝐴 ∈ V
2		f1osn.2	⊢ 𝐵 ∈ V
3	1 2	fnsn	⊢ { ⟨ 𝐴 , 𝐵 ⟩ } Fn { 𝐴 }
4	2 1	fnsn	⊢ { ⟨ 𝐵 , 𝐴 ⟩ } Fn { 𝐵 }
5	1 2	cnvsn	⊢ ◡ { ⟨ 𝐴 , 𝐵 ⟩ } = { ⟨ 𝐵 , 𝐴 ⟩ }
6	5	fneq1i	⊢ ( ◡ { ⟨ 𝐴 , 𝐵 ⟩ } Fn { 𝐵 } ↔ { ⟨ 𝐵 , 𝐴 ⟩ } Fn { 𝐵 } )
7	4 6	mpbir	⊢ ◡ { ⟨ 𝐴 , 𝐵 ⟩ } Fn { 𝐵 }
8		dff1o4	⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 } ↔ ( { ⟨ 𝐴 , 𝐵 ⟩ } Fn { 𝐴 } ∧ ◡ { ⟨ 𝐴 , 𝐵 ⟩ } Fn { 𝐵 } ) )
9	3 7 8	mpbir2an	⊢ { ⟨ 𝐴 , 𝐵 ⟩ } : { 𝐴 } –1-1-onto→ { 𝐵 }