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

Metamath Proof Explorer

Theorem plendxnocndx

Description: The slot for the orthocomplementation is not the slot for the order in an extensible structure. Formerly part of proof for thlle . (Contributed by AV, 11-Nov-2024)

Ref Expression
Assertion plendxnocndx ( le ‘ ndx ) ≠ ( oc ‘ ndx )

Proof

Step Hyp Ref Expression
1 10re ⊢ 1 0 ∈ ℝ
2 1nn0 ⊢ 1 ∈ ℕ0
3 0nn0 ⊢ 0 ∈ ℕ0
4 1nn ⊢ 1 ∈ ℕ
5 0lt1 ⊢ 0 < 1
6 2 3 4 5 declt ⊢ 1 0 < 1 1
7 1 6 ltneii ⊢ 1 0 ≠ 1 1
8 plendx ⊢ ( le ‘ ndx ) = 1 0
9 ocndx ⊢ ( oc ‘ ndx ) = 1 1
10 8 9 neeq12i ⊢ ( ( le ‘ ndx ) ≠ ( oc ‘ ndx ) ↔ 1 0 ≠ 1 1 )
11 7 10 mpbir ⊢ ( le ‘ ndx ) ≠ ( oc ‘ ndx )