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 OL$
	isomli.b	$⊢ B = {Base}_{K}$
	isomli.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	isomli.j	$⊢ \underset{˙}{\lor} = join (K)$
	isomli.m	$⊢ \underset{˙}{\land} = meet (K)$
	isomli.o	$⊢ \underset{˙}{⊥} = oc (K)$
	isomli.7	$⊢ (x \in B \land y \in B) \to (x \underset{˙}{\leq} y \to y = x \underset{˙}{\lor} (y \underset{˙}{\land} \underset{˙}{⊥} (x)))$
Assertion	isomliN	$⊢ K \in OML$

Step	Hyp	Ref	Expression
1		isomli.0	$⊢ K \in OL$
2		isomli.b	$⊢ B = {Base}_{K}$
3		isomli.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
4		isomli.j	$⊢ \underset{˙}{\lor} = join (K)$
5		isomli.m	$⊢ \underset{˙}{\land} = meet (K)$
6		isomli.o	$⊢ \underset{˙}{⊥} = oc (K)$
7		isomli.7	$⊢ (x \in B \land y \in B) \to (x \underset{˙}{\leq} y \to y = x \underset{˙}{\lor} (y \underset{˙}{\land} \underset{˙}{⊥} (x)))$
8	7	rgen2	$⊢ \forall x \in B \forall y \in B (x \underset{˙}{\leq} y \to y = x \underset{˙}{\lor} (y \underset{˙}{\land} \underset{˙}{⊥} (x)))$
9	2 3 4 5 6	isoml	$⊢ K \in OML \leftrightarrow (K \in OL \land \forall x \in B \forall y \in B (x \underset{˙}{\leq} y \to y = x \underset{˙}{\lor} (y \underset{˙}{\land} \underset{˙}{⊥} (x))))$
10	1 8 9	mpbir2an	$⊢ K \in OML$

Metamath Proof Explorer