Theorem islpln

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

	Ref	Expression
Hypotheses	lplnset.b	$$⊢B={\mathrm{Base}}_K$$
	lplnset.c	$$⊢C={⋖}_K$$
	lplnset.n	$$⊢N=\mathrm{LLines}\left(K\right)$$
	lplnset.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
Assertion	islpln	$$⊢K\in A\to \left(X\in P\leftrightarrow \left(X\in B\wedge \exists y\in NyCX\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lplnset.b	$$⊢B={\mathrm{Base}}_K$$
2		lplnset.c	$$⊢C={⋖}_K$$
3		lplnset.n	$$⊢N=\mathrm{LLines}\left(K\right)$$
4		lplnset.p	$$⊢P=\mathrm{LPlanes}\left(K\right)$$
5	1 2 3 4	lplnset	$$⊢K\in A\to P=\left\{x\in B|\exists y\in NyCx\right\}$$
6	5	eleq2d	$$⊢K\in A\to \left(X\in P\leftrightarrow X\in \left\{x\in B|\exists y\in NyCx\right\}\right)$$
7		breq2	$$⊢x=X\to \left(yCx\leftrightarrow yCX\right)$$
8	7	rexbidv	$$⊢x=X\to \left(\exists y\in NyCx\leftrightarrow \exists y\in NyCX\right)$$
9	8	elrab	$$⊢X\in \left\{x\in B|\exists y\in NyCx\right\}\leftrightarrow \left(X\in B\wedge \exists y\in NyCX\right)$$
10	6 9	bitrdi	$$⊢K\in A\to \left(X\in P\leftrightarrow \left(X\in B\wedge \exists y\in NyCX\right)\right)$$