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

Metamath Proof Explorer

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