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

Metamath Proof Explorer

Theorem 1dimN

Description: An atom is covered by a height-2 element (1-dimensional line). (Contributed by NM, 3-May-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2dim.j 
|- .\/ = ( join ` K )
2dim.c 
|- C = (
2dim.a 
|- A = ( Atoms ` K )
Assertion 1dimN 
|- ( ( K e. HL /\ P e. A ) -> E. q e. A P C ( P .\/ q ) )

Proof

Step Hyp Ref Expression
1 2dim.j 
 |-  .\/ = ( join ` K )
2 2dim.c 
 |-  C = (
3 2dim.a 
 |-  A = ( Atoms ` K )
4 1 2 3 2dim 
 |-  ( ( K e. HL /\ P e. A ) -> E. q e. A E. r e. A ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) )
5 r19.42v 
 |-  ( E. r e. A ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) <-> ( P C ( P .\/ q ) /\ E. r e. A ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) )
6 5 simplbi 
 |-  ( E. r e. A ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) -> P C ( P .\/ q ) )
7 6 reximi 
 |-  ( E. q e. A E. r e. A ( P C ( P .\/ q ) /\ ( P .\/ q ) C ( ( P .\/ q ) .\/ r ) ) -> E. q e. A P C ( P .\/ q ) )
8 4 7 syl 
 |-  ( ( K e. HL /\ P e. A ) -> E. q e. A P C ( P .\/ q ) )