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

Metamath Proof Explorer

Theorem islln4

Description: The predicate "is a lattice line". (Contributed by NM, 16-Jun-2012)

	Ref	Expression
Hypotheses	llnset.b	$⊢ B = {Base}_{K}$
	llnset.c	$⊢ C = ⋖_{K}$
	llnset.a	$⊢ A = Atoms (K)$
	llnset.n	$⊢ N = LLines (K)$
Assertion	islln4	$⊢ (K \in D \land X \in B) \to (X \in N \leftrightarrow \exists p \in A p C X)$

Step	Hyp	Ref	Expression
1		llnset.b	$⊢ B = {Base}_{K}$
2		llnset.c	$⊢ C = ⋖_{K}$
3		llnset.a	$⊢ A = Atoms (K)$
4		llnset.n	$⊢ N = LLines (K)$
5	1 2 3 4	islln	$⊢ K \in D \to (X \in N \leftrightarrow (X \in B \land \exists p \in A p C X))$
6	5	baibd	$⊢ (K \in D \land X \in B) \to (X \in N \leftrightarrow \exists p \in A p C X)$