Theorem llni

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

	Ref	Expression
Hypotheses	llnset.b	|- B = ( Base ` K )
	llnset.c	|- C = (
	llnset.a	|- A = ( Atoms ` K )
	llnset.n	|- N = ( LLines ` K )
Assertion	llni	|- ( ( ( K e. D /\ X e. B /\ P e. A ) /\ P C X ) -> X e. N )

Proof

Step	Hyp	Ref	Expression
1		llnset.b	|- B = ( Base ` K )
2		llnset.c	|- C = (
3		llnset.a	|- A = ( Atoms ` K )
4		llnset.n	|- N = ( LLines ` K )
5		simpl2	|- ( ( ( K e. D /\ X e. B /\ P e. A ) /\ P C X ) -> X e. B )
6		breq1	|- ( p = P -> ( p C X <-> P C X ) )
7	6	rspcev	|- ( ( P e. A /\ P C X ) -> E. p e. A p C X )
8	7	3ad2antl3	|- ( ( ( K e. D /\ X e. B /\ P e. A ) /\ P C X ) -> E. p e. A p C X )
9		simpl1	|- ( ( ( K e. D /\ X e. B /\ P e. A ) /\ P C X ) -> K e. D )
10	1 2 3 4	islln	|- ( K e. D -> ( X e. N <-> ( X e. B /\ E. p e. A p C X ) ) )
11	9 10	syl	|- ( ( ( K e. D /\ X e. B /\ P e. A ) /\ P C X ) -> ( X e. N <-> ( X e. B /\ E. p e. A p C X ) ) )
12	5 8 11	mpbir2and	|- ( ( ( K e. D /\ X e. B /\ P e. A ) /\ P C X ) -> X e. N )