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

Metamath Proof Explorer

Theorem slotsdifocndx

Description: The index of the slot for the orthocomplementation is not the index of other slots. Formerly part of proof for prstcocval . (Contributed by AV, 12-Nov-2024)

Ref Expression
Assertion slotsdifocndx ( ( oc ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( oc ‘ ndx ) ≠ ( Hom ‘ ndx ) )

Proof

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