islln2

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

	Ref	Expression
Hypotheses	islln3.b	$⊢ B = {Base}_{K}$
	islln3.j	$⊢ \underset{˙}{\lor} = join (K)$
	islln3.a	$⊢ A = Atoms (K)$
	islln3.n	$⊢ N = LLines (K)$
Assertion	islln2	$⊢ K \in HL \to (X \in N \leftrightarrow (X \in B \land \exists p \in A \exists q \in A (p \neq q \land X = p \underset{˙}{\lor} q)))$

Step	Hyp	Ref	Expression
1		islln3.b	$⊢ B = {Base}_{K}$
2		islln3.j	$⊢ \underset{˙}{\lor} = join (K)$
3		islln3.a	$⊢ A = Atoms (K)$
4		islln3.n	$⊢ N = LLines (K)$
5	1 4	llnbase	$⊢ X \in N \to X \in B$
6	5	pm4.71ri	$⊢ X \in N \leftrightarrow (X \in B \land X \in N)$
7	1 2 3 4	islln3	$⊢ (K \in HL \land X \in B) \to (X \in N \leftrightarrow \exists p \in A \exists q \in A (p \neq q \land X = p \underset{˙}{\lor} q))$
8	7	pm5.32da	$⊢ K \in HL \to ((X \in B \land X \in N) \leftrightarrow (X \in B \land \exists p \in A \exists q \in A (p \neq q \land X = p \underset{˙}{\lor} q)))$
9	6 8	bitrid	$⊢ K \in HL \to (X \in N \leftrightarrow (X \in B \land \exists p \in A \exists q \in A (p \neq q \land X = p \underset{˙}{\lor} q)))$

Metamath Proof Explorer