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	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } )
	f1omptsn.r	⊢ 𝑅 = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } }
Assertion	f1omptsn	⊢ 𝐹 : 𝐴 –1-1-onto→ 𝑅

Proof

Step	Hyp	Ref	Expression
1		f1omptsn.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } )
2		f1omptsn.r	⊢ 𝑅 = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } }
3		sneq	⊢ ( 𝑥 = 𝑎 → { 𝑥 } = { 𝑎 } )
4	3	cbvmptv	⊢ ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } ) = ( 𝑎 ∈ 𝐴 ↦ { 𝑎 } )
5	4	eqcomi	⊢ ( 𝑎 ∈ 𝐴 ↦ { 𝑎 } ) = ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } )
6		id	⊢ ( 𝑢 = 𝑧 → 𝑢 = 𝑧 )
7	6 3	eqeqan12d	⊢ ( ( 𝑢 = 𝑧 ∧ 𝑥 = 𝑎 ) → ( 𝑢 = { 𝑥 } ↔ 𝑧 = { 𝑎 } ) )
8	7	cbvrexdva	⊢ ( 𝑢 = 𝑧 → ( ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } ↔ ∃ 𝑎 ∈ 𝐴 𝑧 = { 𝑎 } ) )
9	8	cbvabv	⊢ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } } = { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = { 𝑎 } }
10	9	eqcomi	⊢ { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = { 𝑎 } } = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } }
11	5 10	f1omptsnlem	⊢ ( 𝑎 ∈ 𝐴 ↦ { 𝑎 } ) : 𝐴 –1-1-onto→ { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = { 𝑎 } }
12	2 9	eqtri	⊢ 𝑅 = { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = { 𝑎 } }
13		f1oeq3	⊢ ( 𝑅 = { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = { 𝑎 } } → ( ( 𝑎 ∈ 𝐴 ↦ { 𝑎 } ) : 𝐴 –1-1-onto→ 𝑅 ↔ ( 𝑎 ∈ 𝐴 ↦ { 𝑎 } ) : 𝐴 –1-1-onto→ { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = { 𝑎 } } ) )
14	12 13	ax-mp	⊢ ( ( 𝑎 ∈ 𝐴 ↦ { 𝑎 } ) : 𝐴 –1-1-onto→ 𝑅 ↔ ( 𝑎 ∈ 𝐴 ↦ { 𝑎 } ) : 𝐴 –1-1-onto→ { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 𝑧 = { 𝑎 } } )
15	11 14	mpbir	⊢ ( 𝑎 ∈ 𝐴 ↦ { 𝑎 } ) : 𝐴 –1-1-onto→ 𝑅
16	1 4	eqtri	⊢ 𝐹 = ( 𝑎 ∈ 𝐴 ↦ { 𝑎 } )
17		f1oeq1	⊢ ( 𝐹 = ( 𝑎 ∈ 𝐴 ↦ { 𝑎 } ) → ( 𝐹 : 𝐴 –1-1-onto→ 𝑅 ↔ ( 𝑎 ∈ 𝐴 ↦ { 𝑎 } ) : 𝐴 –1-1-onto→ 𝑅 ) )
18	16 17	ax-mp	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝑅 ↔ ( 𝑎 ∈ 𝐴 ↦ { 𝑎 } ) : 𝐴 –1-1-onto→ 𝑅 )
19	15 18	mpbir	⊢ 𝐹 : 𝐴 –1-1-onto→ 𝑅