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

Metamath Proof Explorer

Theorem slotsdifplendx2

Description: The index of the slot for the "less than or equal to" ordering is not the index of other slots. Formerly part of proof for prstcleval . (Contributed by AV, 12-Nov-2024)

Ref Expression
Assertion slotsdifplendx2 ( ( le ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( le ‘ ndx ) ≠ ( Hom ‘ ndx ) )

Proof

Step Hyp Ref Expression
1 10re ⊢ 1 0 ∈ ℝ
2 1nn0 ⊢ 1 ∈ ℕ0
3 0nn0 ⊢ 0 ∈ ℕ0
4 5nn ⊢ 5 ∈ ℕ
5 5pos ⊢ 0 < 5
6 2 3 4 5 declt ⊢ 1 0 < 1 5
7 1 6 ltneii ⊢ 1 0 ≠ 1 5
8 plendx ⊢ ( le ‘ ndx ) = 1 0
9 ccondx ⊢ ( comp ‘ ndx ) = 1 5
10 8 9 neeq12i ⊢ ( ( le ‘ ndx ) ≠ ( comp ‘ ndx ) ↔ 1 0 ≠ 1 5 )
11 7 10 mpbir ⊢ ( le ‘ ndx ) ≠ ( comp ‘ ndx )
12 4nn ⊢ 4 ∈ ℕ
13 4pos ⊢ 0 < 4
14 2 3 12 13 declt ⊢ 1 0 < 1 4
15 1 14 ltneii ⊢ 1 0 ≠ 1 4
16 homndx ⊢ ( Hom ‘ ndx ) = 1 4
17 8 16 neeq12i ⊢ ( ( le ‘ ndx ) ≠ ( Hom ‘ ndx ) ↔ 1 0 ≠ 1 4 )
18 15 17 mpbir ⊢ ( le ‘ ndx ) ≠ ( Hom ‘ ndx )
19 11 18 pm3.2i ⊢ ( ( le ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( le ‘ ndx ) ≠ ( Hom ‘ ndx ) )