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 × V ) ∖ ran ( ( V ⊗ E ) △ ( I ⊗ V ) ) ) ⊆ ( V × V )
2		df-rel	⊢ ( Rel ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( I ⊗ V ) ) ) ↔ ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( I ⊗ V ) ) ) ⊆ ( V × V ) )
3	1 2	mpbir	⊢ Rel ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( I ⊗ V ) ) )
4		df-singleton	⊢ Singleton = ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( I ⊗ V ) ) )
5	4	releqi	⊢ ( Rel Singleton ↔ Rel ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( I ⊗ V ) ) ) )
6	3 5	mpbir	⊢ Rel Singleton
7		vex	⊢ 𝑥 ∈ V
8		vex	⊢ 𝑦 ∈ V
9	7 8	brsingle	⊢ ( 𝑥 Singleton 𝑦 ↔ 𝑦 = { 𝑥 } )
10		vex	⊢ 𝑧 ∈ V
11	7 10	brsingle	⊢ ( 𝑥 Singleton 𝑧 ↔ 𝑧 = { 𝑥 } )
12		eqtr3	⊢ ( ( 𝑦 = { 𝑥 } ∧ 𝑧 = { 𝑥 } ) → 𝑦 = 𝑧 )
13	9 11 12	syl2anb	⊢ ( ( 𝑥 Singleton 𝑦 ∧ 𝑥 Singleton 𝑧 ) → 𝑦 = 𝑧 )
14	13	ax-gen	⊢ ∀ 𝑧 ( ( 𝑥 Singleton 𝑦 ∧ 𝑥 Singleton 𝑧 ) → 𝑦 = 𝑧 )
15	14	gen2	⊢ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 Singleton 𝑦 ∧ 𝑥 Singleton 𝑧 ) → 𝑦 = 𝑧 )
16		dffun2	⊢ ( Fun Singleton ↔ ( Rel Singleton ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 Singleton 𝑦 ∧ 𝑥 Singleton 𝑧 ) → 𝑦 = 𝑧 ) ) )
17	6 15 16	mpbir2an	⊢ Fun Singleton
18		eqv	⊢ ( dom Singleton = V ↔ ∀ 𝑥 𝑥 ∈ dom Singleton )
19		eqid	⊢ { 𝑥 } = { 𝑥 }
20		snex	⊢ { 𝑥 } ∈ V
21	7 20	brsingle	⊢ ( 𝑥 Singleton { 𝑥 } ↔ { 𝑥 } = { 𝑥 } )
22	19 21	mpbir	⊢ 𝑥 Singleton { 𝑥 }
23		breq2	⊢ ( 𝑦 = { 𝑥 } → ( 𝑥 Singleton 𝑦 ↔ 𝑥 Singleton { 𝑥 } ) )
24	20 23	spcev	⊢ ( 𝑥 Singleton { 𝑥 } → ∃ 𝑦 𝑥 Singleton 𝑦 )
25	22 24	ax-mp	⊢ ∃ 𝑦 𝑥 Singleton 𝑦
26	7	eldm	⊢ ( 𝑥 ∈ dom Singleton ↔ ∃ 𝑦 𝑥 Singleton 𝑦 )
27	25 26	mpbir	⊢ 𝑥 ∈ 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