This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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