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

Metamath Proof Explorer

Theorem basendxnocndx

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

Ref Expression
Assertion basendxnocndx ( Base ‘ ndx ) ≠ ( oc ‘ ndx )

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 1nn ⊢ 1 ∈ ℕ
3 1nn0 ⊢ 1 ∈ ℕ0
4 1lt10 ⊢ 1 < 1 0
5 2 3 3 4 declti ⊢ 1 < 1 1
6 1 5 ltneii ⊢ 1 ≠ 1 1
7 basendx ⊢ ( Base ‘ ndx ) = 1
8 ocndx ⊢ ( oc ‘ ndx ) = 1 1
9 7 8 neeq12i ⊢ ( ( Base ‘ ndx ) ≠ ( oc ‘ ndx ) ↔ 1 ≠ 1 1 )
10 6 9 mpbir ⊢ ( Base ‘ ndx ) ≠ ( oc ‘ ndx )