Theorem islpln

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

	Ref	Expression
Hypotheses	lplnset.b	|- B = ( Base ` K )
	lplnset.c	|- C = (
	lplnset.n	|- N = ( LLines ` K )
	lplnset.p	|- P = ( LPlanes ` K )
Assertion	islpln	|- ( K e. A -> ( X e. P <-> ( X e. B /\ E. y e. N y C X ) ) )

Proof

Step	Hyp	Ref	Expression
1		lplnset.b	|- B = ( Base ` K )
2		lplnset.c	|- C = (
3		lplnset.n	|- N = ( LLines ` K )
4		lplnset.p	|- P = ( LPlanes ` K )
5	1 2 3 4	lplnset	|- ( K e. A -> P = { x e. B | E. y e. N y C x } )
6	5	eleq2d	|- ( K e. A -> ( X e. P <-> X e. { x e. B | E. y e. N y C x } ) )
7		breq2	|- ( x = X -> ( y C x <-> y C X ) )
8	7	rexbidv	|- ( x = X -> ( E. y e. N y C x <-> E. y e. N y C X ) )
9	8	elrab	|- ( X e. { x e. B | E. y e. N y C x } <-> ( X e. B /\ E. y e. N y C X ) )
10	6 9	bitrdi	|- ( K e. A -> ( X e. P <-> ( X e. B /\ E. y e. N y C X ) ) )