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

Metamath Proof Explorer

Theorem fnsingle

Description: The singleton relationship is a function over the universe. (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion fnsingle 
|- Singleton Fn _V

Proof

Step Hyp Ref Expression
1 difss 
 |-  ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( _I (x) _V ) ) ) C_ ( _V X. _V )
2 df-rel 
 |-  ( Rel ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( _I (x) _V ) ) ) <-> ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( _I (x) _V ) ) ) C_ ( _V X. _V ) )
3 1 2 mpbir 
 |-  Rel ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( _I (x) _V ) ) )
4 df-singleton 
 |-  Singleton = ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( _I (x) _V ) ) )
5 4 releqi 
 |-  ( Rel Singleton <-> Rel ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( _I (x) _V ) ) ) )
6 3 5 mpbir 
 |-  Rel Singleton
7 vex 
 |-  x e. _V
8 vex 
 |-  y e. _V
9 7 8 brsingle 
 |-  ( x Singleton y <-> y = { x } )
10 vex 
 |-  z e. _V
11 7 10 brsingle 
 |-  ( x Singleton z <-> z = { x } )
12 eqtr3 
 |-  ( ( y = { x } /\ z = { x } ) -> y = z )
13 9 11 12 syl2anb 
 |-  ( ( x Singleton y /\ x Singleton z ) -> y = z )
14 13 ax-gen 
 |-  A. z ( ( x Singleton y /\ x Singleton z ) -> y = z )
15 14 gen2 
 |-  A. x A. y A. z ( ( x Singleton y /\ x Singleton z ) -> y = z )
16 dffun2 
 |-  ( Fun Singleton <-> ( Rel Singleton /\ A. x A. y A. z ( ( x Singleton y /\ x Singleton z ) -> y = z ) ) )
17 6 15 16 mpbir2an 
 |-  Fun Singleton
18 eqv 
 |-  ( dom Singleton = _V <-> A. x x e. dom Singleton )
19 eqid 
 |-  { x } = { x }
20 vsnex 
 |-  { x } e. _V
21 7 20 brsingle 
 |-  ( x Singleton { x } <-> { x } = { x } )
22 19 21 mpbir 
 |-  x Singleton { x }
23 breq2 
 |-  ( y = { x } -> ( x Singleton y <-> x Singleton { x } ) )
24 20 23 spcev 
 |-  ( x Singleton { x } -> E. y x Singleton y )
25 22 24 ax-mp 
 |-  E. y x Singleton y
26 7 eldm 
 |-  ( x e. dom Singleton <-> E. y x Singleton y )
27 25 26 mpbir 
 |-  x e. dom Singleton
28 18 27 mpgbir 
 |-  dom Singleton = _V
29 df-fn 
 |-  ( Singleton Fn _V <-> ( Fun Singleton /\ dom Singleton = _V ) )
30 17 28 29 mpbir2an 
 |-  Singleton Fn _V