Theorem f1omptsnlem

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

	Ref	Expression
Hypotheses	f1omptsn.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } )
	f1omptsn.r	⊢ 𝑅 = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } }
Assertion	f1omptsnlem	⊢ 𝐹 : 𝐴 –1-1-onto→ 𝑅

Proof

Step	Hyp	Ref	Expression
1		f1omptsn.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } )
2		f1omptsn.r	⊢ 𝑅 = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } }
3		eqid	⊢ { 𝑥 } = { 𝑥 }
4		snex	⊢ { 𝑥 } ∈ V
5		eqsbc1	⊢ ( { 𝑥 } ∈ V → ( [ { 𝑥 } / 𝑢 ] 𝑢 = { 𝑥 } ↔ { 𝑥 } = { 𝑥 } ) )
6	4 5	ax-mp	⊢ ( [ { 𝑥 } / 𝑢 ] 𝑢 = { 𝑥 } ↔ { 𝑥 } = { 𝑥 } )
7	3 6	mpbir	⊢ [ { 𝑥 } / 𝑢 ] 𝑢 = { 𝑥 }
8		sbcel2	⊢ ( [ { 𝑥 } / 𝑢 ] 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ⦋ { 𝑥 } / 𝑢 ⦌ 𝐴 )
9		csbconstg	⊢ ( { 𝑥 } ∈ V → ⦋ { 𝑥 } / 𝑢 ⦌ 𝐴 = 𝐴 )
10	4 9	ax-mp	⊢ ⦋ { 𝑥 } / 𝑢 ⦌ 𝐴 = 𝐴
11	10	eleq2i	⊢ ( 𝑥 ∈ ⦋ { 𝑥 } / 𝑢 ⦌ 𝐴 ↔ 𝑥 ∈ 𝐴 )
12	8 11	bitri	⊢ ( [ { 𝑥 } / 𝑢 ] 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 )
13	2	abeq2i	⊢ ( 𝑢 ∈ 𝑅 ↔ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } )
14		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) )
15	13 14	sylbbr	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) → 𝑢 ∈ 𝑅 )
16	15	19.23bi	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) → 𝑢 ∈ 𝑅 )
17	16	sbcth	⊢ ( { 𝑥 } ∈ V → [ { 𝑥 } / 𝑢 ] ( ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) → 𝑢 ∈ 𝑅 ) )
18	4 17	ax-mp	⊢ [ { 𝑥 } / 𝑢 ] ( ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) → 𝑢 ∈ 𝑅 )
19		sbcimg	⊢ ( { 𝑥 } ∈ V → ( [ { 𝑥 } / 𝑢 ] ( ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) → 𝑢 ∈ 𝑅 ) ↔ ( [ { 𝑥 } / 𝑢 ] ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) → [ { 𝑥 } / 𝑢 ] 𝑢 ∈ 𝑅 ) ) )
20	4 19	ax-mp	⊢ ( [ { 𝑥 } / 𝑢 ] ( ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) → 𝑢 ∈ 𝑅 ) ↔ ( [ { 𝑥 } / 𝑢 ] ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) → [ { 𝑥 } / 𝑢 ] 𝑢 ∈ 𝑅 ) )
21	18 20	mpbi	⊢ ( [ { 𝑥 } / 𝑢 ] ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) → [ { 𝑥 } / 𝑢 ] 𝑢 ∈ 𝑅 )
22		sbcan	⊢ ( [ { 𝑥 } / 𝑢 ] ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) ↔ ( [ { 𝑥 } / 𝑢 ] 𝑥 ∈ 𝐴 ∧ [ { 𝑥 } / 𝑢 ] 𝑢 = { 𝑥 } ) )
23		sbcel1v	⊢ ( [ { 𝑥 } / 𝑢 ] 𝑢 ∈ 𝑅 ↔ { 𝑥 } ∈ 𝑅 )
24	21 22 23	3imtr3i	⊢ ( ( [ { 𝑥 } / 𝑢 ] 𝑥 ∈ 𝐴 ∧ [ { 𝑥 } / 𝑢 ] 𝑢 = { 𝑥 } ) → { 𝑥 } ∈ 𝑅 )
25	12 24	sylanbr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ [ { 𝑥 } / 𝑢 ] 𝑢 = { 𝑥 } ) → { 𝑥 } ∈ 𝑅 )
26	7 25	mpan2	⊢ ( 𝑥 ∈ 𝐴 → { 𝑥 } ∈ 𝑅 )
27	1 26	fmpti	⊢ 𝐹 : 𝐴 ⟶ 𝑅
28	1	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ { 𝑥 } ∈ 𝑅 ) → ( 𝐹 ‘ 𝑥 ) = { 𝑥 } )
29	26 28	mpdan	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) = { 𝑥 } )
30		sneq	⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
31	30 1 4	fvmpt3i	⊢ ( 𝑦 ∈ 𝐴 → ( 𝐹 ‘ 𝑦 ) = { 𝑦 } )
32	29 31	eqeqan12d	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ { 𝑥 } = { 𝑦 } ) )
33		vex	⊢ 𝑥 ∈ V
34		sneqbg	⊢ ( 𝑥 ∈ V → ( { 𝑥 } = { 𝑦 } ↔ 𝑥 = 𝑦 ) )
35	33 34	ax-mp	⊢ ( { 𝑥 } = { 𝑦 } ↔ 𝑥 = 𝑦 )
36	32 35	bitrdi	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
37	36	biimpd	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
38	37	rgen2	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 )
39		dff13	⊢ ( 𝐹 : 𝐴 –1-1→ 𝑅 ↔ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
40	27 38 39	mpbir2an	⊢ 𝐹 : 𝐴 –1-1→ 𝑅
41		f1f1orn	⊢ ( 𝐹 : 𝐴 –1-1→ 𝑅 → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )
42	40 41	ax-mp	⊢ 𝐹 : 𝐴 –1-1-onto→ ran 𝐹
43		rnmptsn	⊢ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } ) = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } }
44	1	rneqi	⊢ ran 𝐹 = ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } )
45	43 44 2	3eqtr4i	⊢ ran 𝐹 = 𝑅
46		f1oeq3	⊢ ( ran 𝐹 = 𝑅 → ( 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ↔ 𝐹 : 𝐴 –1-1-onto→ 𝑅 ) )
47	45 46	ax-mp	⊢ ( 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ↔ 𝐹 : 𝐴 –1-1-onto→ 𝑅 )
48	42 47	mpbi	⊢ 𝐹 : 𝐴 –1-1-onto→ 𝑅