Theorem islln

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

	Ref	Expression
Hypotheses	llnset.b	$$⊢B={\mathrm{Base}}_K$$
	llnset.c	$$⊢C={⋖}_K$$
	llnset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	llnset.n	$$⊢N=\mathrm{LLines}\left(K\right)$$
Assertion	islln	$$⊢K\in D\to \left(X\in N\leftrightarrow \left(X\in B\wedge \exists p\in ApCX\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		llnset.b	$$⊢B={\mathrm{Base}}_K$$
2		llnset.c	$$⊢C={⋖}_K$$
3		llnset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		llnset.n	$$⊢N=\mathrm{LLines}\left(K\right)$$
5	1 2 3 4	llnset	$$⊢K\in D\to N=\left\{x\in B|\exists p\in ApCx\right\}$$
6	5	eleq2d	$$⊢K\in D\to \left(X\in N\leftrightarrow X\in \left\{x\in B|\exists p\in ApCx\right\}\right)$$
7		breq2	$$⊢x=X\to \left(pCx\leftrightarrow pCX\right)$$
8	7	rexbidv	$$⊢x=X\to \left(\exists p\in ApCx\leftrightarrow \exists p\in ApCX\right)$$
9	8	elrab	$$⊢X\in \left\{x\in B|\exists p\in ApCx\right\}\leftrightarrow \left(X\in B\wedge \exists p\in ApCX\right)$$
10	6 9	bitrdi	$$⊢K\in D\to \left(X\in N\leftrightarrow \left(X\in B\wedge \exists p\in ApCX\right)\right)$$