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 ^◡ { ⟨ 𝐴 , 𝐵 ⟩ }

Proof

Step	Hyp	Ref	Expression
1		relcnv	⊢ Rel ^◡ { ⟨ 𝐴 , 𝐵 ⟩ }
2		moeq	⊢ ∃* 𝑦 𝑦 = 𝐴
3		vex	⊢ 𝑥 ∈ V
4		vex	⊢ 𝑦 ∈ V
5	3 4	brcnv	⊢ ( 𝑥 ^◡ { ⟨ 𝐴 , 𝐵 ⟩ } 𝑦 ↔ 𝑦 { ⟨ 𝐴 , 𝐵 ⟩ } 𝑥 )
6		df-br	⊢ ( 𝑦 { ⟨ 𝐴 , 𝐵 ⟩ } 𝑥 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } )
7	5 6	bitri	⊢ ( 𝑥 ^◡ { ⟨ 𝐴 , 𝐵 ⟩ } 𝑦 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } )
8		elsni	⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } → ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
9	4 3	opth1	⊢ ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ → 𝑦 = 𝐴 )
10	8 9	syl	⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } → 𝑦 = 𝐴 )
11	7 10	sylbi	⊢ ( 𝑥 ^◡ { ⟨ 𝐴 , 𝐵 ⟩ } 𝑦 → 𝑦 = 𝐴 )
12	11	moimi	⊢ ( ∃* 𝑦 𝑦 = 𝐴 → ∃* 𝑦 𝑥 ^◡ { ⟨ 𝐴 , 𝐵 ⟩ } 𝑦 )
13	2 12	ax-mp	⊢ ∃* 𝑦 𝑥 ^◡ { ⟨ 𝐴 , 𝐵 ⟩ } 𝑦
14	13	ax-gen	⊢ ∀ 𝑥 ∃* 𝑦 𝑥 ^◡ { ⟨ 𝐴 , 𝐵 ⟩ } 𝑦
15		dffun6	⊢ ( Fun ^◡ { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ( Rel ^◡ { ⟨ 𝐴 , 𝐵 ⟩ } ∧ ∀ 𝑥 ∃* 𝑦 𝑥 ^◡ { ⟨ 𝐴 , 𝐵 ⟩ } 𝑦 ) )
16	1 14 15	mpbir2an	⊢ Fun ^◡ { ⟨ 𝐴 , 𝐵 ⟩ }