This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )