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	$⊢ \leq_{ndx} \neq oc (ndx)$

Proof

Step	Hyp	Ref	Expression
1		10re	$⊢ 10 \in ℝ$
2		1nn0	$⊢ 1 \in ℕ_{0}$
3		0nn0	$⊢ 0 \in ℕ_{0}$
4		1nn	$⊢ 1 \in ℕ$
5		0lt1	$⊢ 0 < 1$
6	2 3 4 5	declt	$⊢ 10 < 11$
7	1 6	ltneii	$⊢ 10 \neq 11$
8		plendx	$⊢ \leq_{ndx} = 10$
9		ocndx	$⊢ oc (ndx) = 11$
10	8 9	neeq12i	$⊢ \leq_{ndx} \neq oc (ndx) \leftrightarrow 10 \neq 11$
11	7 10	mpbir	$⊢ \leq_{ndx} \neq oc (ndx)$