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 >. }

Proof

Step Hyp Ref Expression
1 relcnv 
 |-  Rel `' { <. A , B >. }
2 moeq 
 |-  E* y y = A
3 vex 
 |-  x e. _V
4 vex 
 |-  y e. _V
5 3 4 brcnv 
 |-  ( x `' { <. A , B >. } y <-> y { <. A , B >. } x )
6 df-br 
 |-  ( y { <. A , B >. } x <-> <. y , x >. e. { <. A , B >. } )
7 5 6 bitri 
 |-  ( x `' { <. A , B >. } y <-> <. y , x >. e. { <. A , B >. } )
8 elsni 
 |-  ( <. y , x >. e. { <. A , B >. } -> <. y , x >. = <. A , B >. )
9 4 3 opth1 
 |-  ( <. y , x >. = <. A , B >. -> y = A )
10 8 9 syl 
 |-  ( <. y , x >. e. { <. A , B >. } -> y = A )
11 7 10 sylbi 
 |-  ( x `' { <. A , B >. } y -> y = A )
12 11 moimi 
 |-  ( E* y y = A -> E* y x `' { <. A , B >. } y )
13 2 12 ax-mp 
 |-  E* y x `' { <. A , B >. } y
14 13 ax-gen 
 |-  A. x E* y x `' { <. A , B >. } y
15 dffun6 
 |-  ( Fun `' { <. A , B >. } <-> ( Rel `' { <. A , B >. } /\ A. x E* y x `' { <. A , B >. } y ) )
16 1 14 15 mpbir2an 
 |-  Fun `' { <. A , B >. }