Theorem isomliN

Description: Properties that determine an orthomodular lattice. (Contributed by NM, 18-Sep-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	isomli.0	$$⊢K\in \mathrm{OL}$$
	isomli.b	$$⊢B={\mathrm{Base}}_K$$
	isomli.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	isomli.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	isomli.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	isomli.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
	isomli.7	$$⊢\left(x\in B\wedge y\in B\right)\to \left(x\underset{\dot{}}{\le }y\to y=x\underset{\dot{}}{\vee }\left(y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)\right)\right)$$
Assertion	isomliN	$$⊢K\in \mathrm{OML}$$

Proof

Step	Hyp	Ref	Expression
1		isomli.0	$$⊢K\in \mathrm{OL}$$
2		isomli.b	$$⊢B={\mathrm{Base}}_K$$
3		isomli.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
4		isomli.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
5		isomli.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
6		isomli.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
7		isomli.7	$$⊢\left(x\in B\wedge y\in B\right)\to \left(x\underset{\dot{}}{\le }y\to y=x\underset{\dot{}}{\vee }\left(y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)\right)\right)$$
8	7	rgen2	$$⊢\forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\to y=x\underset{\dot{}}{\vee }\left(y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)\right)\right)$$
9	2 3 4 5 6	isoml	$$⊢K\in \mathrm{OML}\leftrightarrow \left(K\in \mathrm{OL}\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\to y=x\underset{\dot{}}{\vee }\left(y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)\right)\right)\right)$$
10	1 8 9	mpbir2an	$$⊢K\in \mathrm{OML}$$