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

Metamath Proof Explorer

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	$⊢ A \in V$
		f1osn.2	$⊢ B \in V$
	Assertion	f1osn	$⊢ \{⟨A, B⟩\} : \{A\} \underset{1-1 onto}{⟶} \{B\}$

Proof

Step	Hyp	Ref	Expression
1		f1osn.1	$⊢ A \in V$
2		f1osn.2	$⊢ B \in V$
3	1 2	fnsn	$⊢ \{⟨A, B⟩\} Fn \{A\}$
4	2 1	fnsn	$⊢ \{⟨B, A⟩\} Fn \{B\}$
5	1 2	cnvsn	$⊢ {\{⟨A, B⟩\}}^{-1} = \{⟨B, A⟩\}$
6	5	fneq1i	$⊢ {\{⟨A, B⟩\}}^{-1} Fn \{B\} \leftrightarrow \{⟨B, A⟩\} Fn \{B\}$
7	4 6	mpbir	$⊢ {\{⟨A, B⟩\}}^{-1} Fn \{B\}$
8		dff1o4	$⊢ \{⟨A, B⟩\} : \{A\} \underset{1-1 onto}{⟶} \{B\} \leftrightarrow (\{⟨A, B⟩\} Fn \{A\} \land {\{⟨A, B⟩\}}^{-1} Fn \{B\})$
9	3 7 8	mpbir2an	$⊢ \{⟨A, B⟩\} : \{A\} \underset{1-1 onto}{⟶} \{B\}$