Theorem nf1oconst

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

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

Proof

Step	Hyp	Ref	Expression
1		nf1const	⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) ) → ¬ 𝐹 : 𝐴 –1-1→ 𝐶 )
2	1	orcd	⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) ) → ( ¬ 𝐹 : 𝐴 –1-1→ 𝐶 ∨ ¬ 𝐹 : 𝐴 –onto→ 𝐶 ) )
3		ianor	⊢ ( ¬ ( 𝐹 : 𝐴 –1-1→ 𝐶 ∧ 𝐹 : 𝐴 –onto→ 𝐶 ) ↔ ( ¬ 𝐹 : 𝐴 –1-1→ 𝐶 ∨ ¬ 𝐹 : 𝐴 –onto→ 𝐶 ) )
4		df-f1o	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐶 ↔ ( 𝐹 : 𝐴 –1-1→ 𝐶 ∧ 𝐹 : 𝐴 –onto→ 𝐶 ) )
5	3 4	xchnxbir	⊢ ( ¬ 𝐹 : 𝐴 –1-1-onto→ 𝐶 ↔ ( ¬ 𝐹 : 𝐴 –1-1→ 𝐶 ∨ ¬ 𝐹 : 𝐴 –onto→ 𝐶 ) )
6	2 5	sylibr	⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) ) → ¬ 𝐹 : 𝐴 –1-1-onto→ 𝐶 )