llni

Description: Condition implying a lattice line. (Contributed by NM, 17-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	llni	$⊢ ((K \in D \land X \in B \land P \in A) \land P C X) \to X \in N$

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		simpl2	$⊢ ((K \in D \land X \in B \land P \in A) \land P C X) \to X \in B$
6		breq1	$⊢ p = P \to (p C X \leftrightarrow P C X)$
7	6	rspcev	$⊢ (P \in A \land P C X) \to \exists p \in A p C X$
8	7	3ad2antl3	$⊢ ((K \in D \land X \in B \land P \in A) \land P C X) \to \exists p \in A p C X$
9		simpl1	$⊢ ((K \in D \land X \in B \land P \in A) \land P C X) \to K \in D$
10	1 2 3 4	islln	$⊢ K \in D \to (X \in N \leftrightarrow (X \in B \land \exists p \in A p C X))$
11	9 10	syl	$⊢ ((K \in D \land X \in B \land P \in A) \land P C X) \to (X \in N \leftrightarrow (X \in B \land \exists p \in A p C X))$
12	5 8 11	mpbir2and	$⊢ ((K \in D \land X \in B \land P \in A) \land P C X) \to X \in N$

Metamath Proof Explorer