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	$⊢ (A \in V \land B \in W) \to \{⟨A, B⟩\} : \{A\} \underset{1-1 onto}{⟶} \{B\}$

Step	Hyp	Ref	Expression
1		sneq	$⊢ a = A \to \{a\} = \{A\}$
2	1	f1oeq2d	$⊢ a = A \to (\{⟨a, b⟩\} : \{a\} \underset{1-1 onto}{⟶} \{b\} \leftrightarrow \{⟨a, b⟩\} : \{A\} \underset{1-1 onto}{⟶} \{b\})$
3		opeq1	$⊢ a = A \to ⟨a, b⟩ = ⟨A, b⟩$
4	3	sneqd	$⊢ a = A \to \{⟨a, b⟩\} = \{⟨A, b⟩\}$
5	4	f1oeq1d	$⊢ a = A \to (\{⟨a, b⟩\} : \{A\} \underset{1-1 onto}{⟶} \{b\} \leftrightarrow \{⟨A, b⟩\} : \{A\} \underset{1-1 onto}{⟶} \{b\})$
6	2 5	bitrd	$⊢ a = A \to (\{⟨a, b⟩\} : \{a\} \underset{1-1 onto}{⟶} \{b\} \leftrightarrow \{⟨A, b⟩\} : \{A\} \underset{1-1 onto}{⟶} \{b\})$
7		sneq	$⊢ b = B \to \{b\} = \{B\}$
8	7	f1oeq3d	$⊢ b = B \to (\{⟨A, b⟩\} : \{A\} \underset{1-1 onto}{⟶} \{b\} \leftrightarrow \{⟨A, b⟩\} : \{A\} \underset{1-1 onto}{⟶} \{B\})$
9		opeq2	$⊢ b = B \to ⟨A, b⟩ = ⟨A, B⟩$
10	9	sneqd	$⊢ b = B \to \{⟨A, b⟩\} = \{⟨A, B⟩\}$
11	10	f1oeq1d	$⊢ b = B \to (\{⟨A, b⟩\} : \{A\} \underset{1-1 onto}{⟶} \{B\} \leftrightarrow \{⟨A, B⟩\} : \{A\} \underset{1-1 onto}{⟶} \{B\})$
12	8 11	bitrd	$⊢ b = B \to (\{⟨A, b⟩\} : \{A\} \underset{1-1 onto}{⟶} \{b\} \leftrightarrow \{⟨A, B⟩\} : \{A\} \underset{1-1 onto}{⟶} \{B\})$
13		vex	$⊢ a \in V$
14		vex	$⊢ b \in V$
15	13 14	f1osn	$⊢ \{⟨a, b⟩\} : \{a\} \underset{1-1 onto}{⟶} \{b\}$
16	6 12 15	vtocl2g	$⊢ (A \in V \land B \in W) \to \{⟨A, B⟩\} : \{A\} \underset{1-1 onto}{⟶} \{B\}$

Metamath Proof Explorer