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

Metamath Proof Explorer

Theorem funcnvsn

Description: The converse singleton of an ordered pair is a function. This is equivalent to funsn via cnvsn , but stating it this way allows to skip the sethood assumptions on A and B . (Contributed by NM, 30-Apr-2015)

		Ref	Expression
	Assertion	funcnvsn	$⊢ Fun {\{⟨A, B⟩\}}^{-1}$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$⊢ Rel {\{⟨A, B⟩\}}^{-1}$
2		moeq	$⊢ \exists^{*} y y = A$
3		vex	$⊢ x \in V$
4		vex	$⊢ y \in V$
5	3 4	brcnv	$⊢ x {\{⟨A, B⟩\}}^{-1} y \leftrightarrow y \{⟨A, B⟩\} x$
6		df-br	$⊢ y \{⟨A, B⟩\} x \leftrightarrow ⟨y, x⟩ \in \{⟨A, B⟩\}$
7	5 6	bitri	$⊢ x {\{⟨A, B⟩\}}^{-1} y \leftrightarrow ⟨y, x⟩ \in \{⟨A, B⟩\}$
8		elsni	$⊢ ⟨y, x⟩ \in \{⟨A, B⟩\} \to ⟨y, x⟩ = ⟨A, B⟩$
9	4 3	opth1	$⊢ ⟨y, x⟩ = ⟨A, B⟩ \to y = A$
10	8 9	syl	$⊢ ⟨y, x⟩ \in \{⟨A, B⟩\} \to y = A$
11	7 10	sylbi	$⊢ x {\{⟨A, B⟩\}}^{-1} y \to y = A$
12	11	moimi	$⊢ \exists^{} y y = A \to \exists^{} y x {\{⟨A, B⟩\}}^{-1} y$
13	2 12	ax-mp	$⊢ \exists^{*} y x {\{⟨A, B⟩\}}^{-1} y$
14	13	ax-gen	$⊢ \forall x \exists^{*} y x {\{⟨A, B⟩\}}^{-1} y$
15		dffun6	$⊢ Fun {\{⟨A, B⟩\}}^{-1} \leftrightarrow (Rel {\{⟨A, B⟩\}}^{-1} \land \forall x \exists^{*} y x {\{⟨A, B⟩\}}^{-1} y)$
16	1 14 15	mpbir2an	$⊢ Fun {\{⟨A, B⟩\}}^{-1}$