Theorem f1cdmsn

Description: If a one-to-one function with a nonempty domain has a singleton as its codomain, its domain must also be a singleton. (Contributed by BTernaryTau, 1-Dec-2024)

	Ref	Expression
Assertion	f1cdmsn	⊢ ( ( 𝐹 : 𝐴 –1-1→ { 𝐵 } ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 𝐴 = { 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		f1f	⊢ ( 𝐹 : 𝐴 –1-1→ { 𝐵 } → 𝐹 : 𝐴 ⟶ { 𝐵 } )
2		fvconst	⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = 𝐵 )
3	2	3adant3	⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = 𝐵 )
4		fvconst	⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) = 𝐵 )
5	4	3adant2	⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) = 𝐵 )
6	3 5	eqtr4d	⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) )
7	1 6	syl3an1	⊢ ( ( 𝐹 : 𝐴 –1-1→ { 𝐵 } ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) )
8		f1veqaeq	⊢ ( ( 𝐹 : 𝐴 –1-1→ { 𝐵 } ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
9	8	3impb	⊢ ( ( 𝐹 : 𝐴 –1-1→ { 𝐵 } ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
10	7 9	mpd	⊢ ( ( 𝐹 : 𝐴 –1-1→ { 𝐵 } ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → 𝑦 = 𝑧 )
11	10	3expia	⊢ ( ( 𝐹 : 𝐴 –1-1→ { 𝐵 } ∧ 𝑦 ∈ 𝐴 ) → ( 𝑧 ∈ 𝐴 → 𝑦 = 𝑧 ) )
12	11	ralrimiv	⊢ ( ( 𝐹 : 𝐴 –1-1→ { 𝐵 } ∧ 𝑦 ∈ 𝐴 ) → ∀ 𝑧 ∈ 𝐴 𝑦 = 𝑧 )
13	12	reximdva0	⊢ ( ( 𝐹 : 𝐴 –1-1→ { 𝐵 } ∧ 𝐴 ≠ ∅ ) → ∃ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 𝑦 = 𝑧 )
14		issn	⊢ ( ∃ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 𝑦 = 𝑧 → ∃ 𝑥 𝐴 = { 𝑥 } )
15	13 14	syl	⊢ ( ( 𝐹 : 𝐴 –1-1→ { 𝐵 } ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 𝐴 = { 𝑥 } )