Theorem f1omptsn

Description: A function mapping to singletons is bijective onto a set of singletons. (Contributed by ML, 16-Jul-2020)

	Ref	Expression
Hypotheses	f1omptsn.f	|- F = ( x e. A |-> { x } )
	f1omptsn.r	|- R = { u | E. x e. A u = { x } }
Assertion	f1omptsn	|- F : A -1-1-onto-> R

Proof

Step	Hyp	Ref	Expression
1		f1omptsn.f	|- F = ( x e. A |-> { x } )
2		f1omptsn.r	|- R = { u | E. x e. A u = { x } }
3		sneq	|- ( x = a -> { x } = { a } )
4	3	cbvmptv	|- ( x e. A |-> { x } ) = ( a e. A |-> { a } )
5	4	eqcomi	|- ( a e. A |-> { a } ) = ( x e. A |-> { x } )
6		id	|- ( u = z -> u = z )
7	6 3	eqeqan12d	|- ( ( u = z /\ x = a ) -> ( u = { x } <-> z = { a } ) )
8	7	cbvrexdva	|- ( u = z -> ( E. x e. A u = { x } <-> E. a e. A z = { a } ) )
9	8	cbvabv	|- { u | E. x e. A u = { x } } = { z | E. a e. A z = { a } }
10	9	eqcomi	|- { z | E. a e. A z = { a } } = { u | E. x e. A u = { x } }
11	5 10	f1omptsnlem	|- ( a e. A |-> { a } ) : A -1-1-onto-> { z | E. a e. A z = { a } }
12	2 9	eqtri	|- R = { z | E. a e. A z = { a } }
13		f1oeq3	|- ( R = { z | E. a e. A z = { a } } -> ( ( a e. A |-> { a } ) : A -1-1-onto-> R <-> ( a e. A |-> { a } ) : A -1-1-onto-> { z | E. a e. A z = { a } } ) )
14	12 13	ax-mp	|- ( ( a e. A |-> { a } ) : A -1-1-onto-> R <-> ( a e. A |-> { a } ) : A -1-1-onto-> { z | E. a e. A z = { a } } )
15	11 14	mpbir	|- ( a e. A |-> { a } ) : A -1-1-onto-> R
16	1 4	eqtri	|- F = ( a e. A |-> { a } )
17		f1oeq1	|- ( F = ( a e. A |-> { a } ) -> ( F : A -1-1-onto-> R <-> ( a e. A |-> { a } ) : A -1-1-onto-> R ) )
18	16 17	ax-mp	|- ( F : A -1-1-onto-> R <-> ( a e. A |-> { a } ) : A -1-1-onto-> R )
19	15 18	mpbir	|- F : A -1-1-onto-> R