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 ⊢ ≤ ndx ≠ comp ⁡ ndx ∧ ≤ ndx ≠ Hom ⁡ ndx

Proof

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