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→ 𝐶 )