Theorem f1omptsnlem 31782

Description: This is the core of the proof of f1omptsn 31783, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 15-Jul-2020.)

Hypotheses

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

Assertion

Ref	Expression
f1omptsnlem	|- F : A -1-1-onto-> R

Distinct variable groups:   x, A, u   x, F   u, R, x

Allowed substitution hint:   F( u)

Proof of Theorem f1omptsnlem

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1omptsn.f	. . . . 5 |- F = ( x e. A |-> { x } )
2		eqid 2461	. . . . . . 7 |- { x } = { x }
3		snex 4654	. . . . . . . 8 |- { x } e. _V
4		eqsbc3 3318	. . . . . . . 8 |- ( { x } e. _V -> ( [. { x } / u ]. u = { x } <-> { x } = { x } ) )
5	3, 4	ax-mp 5	. . . . . . 7 |- ( [. { x } / u ]. u = { x } <-> { x } = { x } )
6	2, 5	mpbir 214	. . . . . 6 |- [. { x } / u ]. u = { x }
7		sbcel2 3789	. . . . . . . 8 |- ( [. { x } / u ]. x e. A <-> x e. [_ { x } / u ]_ A )
8		csbconstg 3387	. . . . . . . . . 10 |- ( { x } e. _V -> [_ { x } / u ]_ A = A )
9	3, 8	ax-mp 5	. . . . . . . . 9 |- [_ { x } / u ]_ A = A
10	9	eleq2i 2531	. . . . . . . 8 |- ( x e. [_ { x } / u ]_ A <-> x e. A )
11	7, 10	bitri 257	. . . . . . 7 |- ( [. { x } / u ]. x e. A <-> x e. A )
12		df-rex 2754	. . . . . . . . . . . . 13 |- ( E. x e. A u = { x } <-> E. x ( x e. A /\ u = { x } ) )
13		f1omptsn.r	. . . . . . . . . . . . . . 15 |- R = { u | E. x e. A u = { x } }
14	13	abeq2i 2573	. . . . . . . . . . . . . 14 |- ( u e. R <-> E. x e. A u = { x } )
15	14	biimpri 211	. . . . . . . . . . . . 13 |- ( E. x e. A u = { x } -> u e. R )
16	12, 15	sylbir 218	. . . . . . . . . . . 12 |- ( E. x ( x e. A /\ u = { x } ) -> u e. R )
17	16	19.23bi 1959	. . . . . . . . . . 11 |- ( ( x e. A /\ u = { x } ) -> u e. R )
18	17	sbcth 3293	. . . . . . . . . 10 |- ( { x } e. _V -> [. { x } / u ]. ( ( x e. A /\ u = { x } ) -> u e. R ) )
19	3, 18	ax-mp 5	. . . . . . . . 9 |- [. { x } / u ]. ( ( x e. A /\ u = { x } ) -> u e. R )
20		sbcimg 3320	. . . . . . . . . 10 |- ( { x } e. _V -> ( [. { x } / u ]. ( ( x e. A /\ u = { x } ) -> u e. R ) <-> ( [. { x } / u ]. ( x e. A /\ u = { x } ) -> [. { x } / u ]. u e. R ) ) )
21	3, 20	ax-mp 5	. . . . . . . . 9 |- ( [. { x } / u ]. ( ( x e. A /\ u = { x } ) -> u e. R ) <-> ( [. { x } / u ]. ( x e. A /\ u = { x } ) -> [. { x } / u ]. u e. R ) )
22	19, 21	mpbi 213	. . . . . . . 8 |- ( [. { x } / u ]. ( x e. A /\ u = { x } ) -> [. { x } / u ]. u e. R )
23		sbcan 3321	. . . . . . . 8 |- ( [. { x } / u ]. ( x e. A /\ u = { x } ) <-> ( [. { x } / u ]. x e. A /\ [. { x } / u ]. u = { x } ) )
24		sbcel1v 3337	. . . . . . . 8 |- ( [. { x } / u ]. u e. R <-> { x } e. R )
25	22, 23, 24	3imtr3i 273	. . . . . . 7 |- ( ( [. { x } / u ]. x e. A /\ [. { x } / u ]. u = { x } ) -> { x } e. R )
26	11, 25	sylanbr 480	. . . . . 6 |- ( ( x e. A /\ [. { x } / u ]. u = { x } ) -> { x } e. R )
27	6, 26	mpan2 682	. . . . 5 |- ( x e. A -> { x } e. R )
28	1, 27	fmpti 6067	. . . 4 |- F : A --> R
29	1	fvmpt2 5979	. . . . . . . . 9 |- ( ( x e. A /\ { x } e. R ) -> ( F ` x ) = { x } )
30	27, 29	mpdan 679	. . . . . . . 8 |- ( x e. A -> ( F ` x ) = { x } )
31		sneq 3989	. . . . . . . . 9 |- ( x = y -> { x } = { y } )
32	31, 1, 3	fvmpt3i 5975	. . . . . . . 8 |- ( y e. A -> ( F ` y ) = { y } )
33	30, 32	eqeqan12d 2477	. . . . . . 7 |- ( ( x e. A /\ y e. A ) -> ( ( F ` x ) = ( F ` y ) <-> { x } = { y } ) )
34		vex 3059	. . . . . . . 8 |- x e. _V
35		sneqbg 4154	. . . . . . . 8 |- ( x e. _V -> ( { x } = { y } <-> x = y ) )
36	34, 35	ax-mp 5	. . . . . . 7 |- ( { x } = { y } <-> x = y )
37	33, 36	syl6bb 269	. . . . . 6 |- ( ( x e. A /\ y e. A ) -> ( ( F ` x ) = ( F ` y ) <-> x = y ) )
38	37	biimpd 212	. . . . 5 |- ( ( x e. A /\ y e. A ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
39	38	rgen2a 2826	. . . 4 |- A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y )
40		dff13 6183	. . . 4 |- ( F : A -1-1-> R <-> ( F : A --> R /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
41	28, 39, 40	mpbir2an 936	. . 3 |- F : A -1-1-> R
42		f1f1orn 5847	. . 3 |- ( F : A -1-1-> R -> F : A -1-1-onto-> ran F )
43	41, 42	ax-mp 5	. 2 |- F : A -1-1-onto-> ran F
44		rnmptsn 31781	. . . 4 |- ran ( x e. A |-> { x } ) = { u | E. x e. A u = { x } }
45	1	rneqi 5079	. . . 4 |- ran F = ran ( x e. A |-> { x } )
46	44, 45, 13	3eqtr4i 2493	. . 3 |- ran F = R
47		f1oeq3 5829	. . 3 |- ( ran F = R -> ( F : A -1-1-onto-> ran F <-> F : A -1-1-onto-> R ) )
48	46, 47	ax-mp 5	. 2 |- ( F : A -1-1-onto-> ran F <-> F : A -1-1-onto-> R )
49	43, 48	mpbi 213	1 |- F : A -1-1-onto-> R

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1454   E.wex 1673   e. wcel 1897   {cab 2447   A.wral 2748   E.wrex 2749   _Vcvv 3056   [.wsbc 3278   [_csb 3374   {csn 3979   |-> cmpt 4474   ran crn 4853   -->wf 5596   -1-1->wf1 5597   -1-1-onto->wf1o 5599   ` cfv 5600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-fal 1460  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-br 4416  df-opab 4475  df-mpt 4476  df-id 4767  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608

This theorem is referenced by:  f1omptsn  31783