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

Metamath Proof Explorer

Theorem nf1const

Description: A constant function from at least two elements is not one-to-one. (Contributed by AV, 30-Mar-2024)

Ref Expression
Assertion nf1const ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) ) → ¬ 𝐹 : 𝐴 –1-1→ 𝐶 )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ∈ 𝐴 )
2 simp2 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) → 𝑌 ∈ 𝐴 )
3 fvconst ⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) = 𝐵 )
4 1 3 sylan2 ⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝐵 )
5 fvconst ⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝑌 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑌 ) = 𝐵 )
6 2 5 sylan2 ⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝐹 ‘ 𝑌 ) = 𝐵 )
7 4 6 eqtr4d ⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) )
8 neneq ⊢ ( 𝑋 ≠ 𝑌 → ¬ 𝑋 = 𝑌 )
9 8 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) → ¬ 𝑋 = 𝑌 )
10 9 adantl ⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) ) → ¬ 𝑋 = 𝑌 )
11 7 10 jcnd ⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) ) → ¬ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) )
12 fveqeq2 ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) ) )
13 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = 𝑦 ↔ 𝑋 = 𝑦 ) )
14 12 13 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) → 𝑋 = 𝑦 ) ) )
15 14 notbid ⊢ ( 𝑥 = 𝑋 → ( ¬ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ¬ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) → 𝑋 = 𝑦 ) ) )
16 fveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑌 ) )
17 16 eqeq2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) )
18 eqeq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 = 𝑦 ↔ 𝑋 = 𝑌 ) )
19 17 18 imbi12d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) → 𝑋 = 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) )
20 19 notbid ⊢ ( 𝑦 = 𝑌 → ( ¬ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑦 ) → 𝑋 = 𝑦 ) ↔ ¬ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) )
21 15 20 rspc2ev ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ ¬ ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) → 𝑋 = 𝑌 ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ¬ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
22 1 2 11 21 syl2an23an ⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ¬ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
23 rexnal2 ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ¬ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
24 22 23 sylib ⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) ) → ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
25 24 olcd ⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) ) → ( ¬ 𝐹 : 𝐴 ⟶ 𝐶 ∨ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
26 ianor ⊢ ( ¬ ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ↔ ( ¬ 𝐹 : 𝐴 ⟶ 𝐶 ∨ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
27 dff13 ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐶 ↔ ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
28 26 27 xchnxbir ⊢ ( ¬ 𝐹 : 𝐴 –1-1→ 𝐶 ↔ ( ¬ 𝐹 : 𝐴 ⟶ 𝐶 ∨ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
29 25 28 sylibr ⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) ) → ¬ 𝐹 : 𝐴 –1-1→ 𝐶 )