Theorem lplni

Description: Condition implying a lattice plane. (Contributed by NM, 20-Jun-2012)

	Ref	Expression
Hypotheses	lplnset.b	|- B = ( Base ` K )
	lplnset.c	|- C = (
	lplnset.n	|- N = ( LLines ` K )
	lplnset.p	|- P = ( LPlanes ` K )
Assertion	lplni	|- ( ( ( K e. D /\ Y e. B /\ X e. N ) /\ X C Y ) -> Y e. P )

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		simpl2	|- ( ( ( K e. D /\ Y e. B /\ X e. N ) /\ X C Y ) -> Y e. B )
6		breq1	|- ( x = X -> ( x C Y <-> X C Y ) )
7	6	rspcev	|- ( ( X e. N /\ X C Y ) -> E. x e. N x C Y )
8	7	3ad2antl3	|- ( ( ( K e. D /\ Y e. B /\ X e. N ) /\ X C Y ) -> E. x e. N x C Y )
9		simpl1	|- ( ( ( K e. D /\ Y e. B /\ X e. N ) /\ X C Y ) -> K e. D )
10	1 2 3 4	islpln	|- ( K e. D -> ( Y e. P <-> ( Y e. B /\ E. x e. N x C Y ) ) )
11	9 10	syl	|- ( ( ( K e. D /\ Y e. B /\ X e. N ) /\ X C Y ) -> ( Y e. P <-> ( Y e. B /\ E. x e. N x C Y ) ) )
12	5 8 11	mpbir2and	|- ( ( ( K e. D /\ Y e. B /\ X e. N ) /\ X C Y ) -> Y e. P )