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		snex	|- { 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