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 }_{\mathrm{ndx}}\ne \mathrm{oc}\left(\mathrm{ndx}\right)$$

Proof

Step	Hyp	Ref	Expression
1		10re	$$⊢10\in ℝ$$
2		1nn0	$$⊢1\in {\mathbb{N}}_0$$
3		0nn0	$$⊢0\in {\mathbb{N}}_0$$
4		1nn	$$⊢1\in \mathbb{N}$$
5		0lt1	$$⊢0<1$$
6	2 3 4 5	declt	$$⊢10<11$$
7	1 6	ltneii	$$⊢10\ne 11$$
8		plendx	$$⊢{\le }_{\mathrm{ndx}}=10$$
9		ocndx	$$⊢\mathrm{oc}\left(\mathrm{ndx}\right)=11$$
10	8 9	neeq12i	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{oc}\left(\mathrm{ndx}\right)\leftrightarrow 10\ne 11$$
11	7 10	mpbir	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{oc}\left(\mathrm{ndx}\right)$$