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 ) )