Metamath Proof Explorer


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→ { 𝐵 } ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 𝐴 = { 𝑥 } )