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	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	2dim.c	$$⊢C={⋖}_K$$
	2dim.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	1dimN	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\right)\to \exists q\in APC\left(P\underset{\dot{}}{\vee }q\right)$$

Proof

Step	Hyp	Ref	Expression
1		2dim.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
2		2dim.c	$$⊢C={⋖}_K$$
3		2dim.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4	1 2 3	2dim	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\right)\to \exists q\in A\exists r\in A\left(PC\left(P\underset{\dot{}}{\vee }q\right)\wedge \left(P\underset{\dot{}}{\vee }q\right)C\left(\left(P\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
5		r19.42v	$$⊢\exists r\in A\left(PC\left(P\underset{\dot{}}{\vee }q\right)\wedge \left(P\underset{\dot{}}{\vee }q\right)C\left(\left(P\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\leftrightarrow \left(PC\left(P\underset{\dot{}}{\vee }q\right)\wedge \exists r\in A\left(P\underset{\dot{}}{\vee }q\right)C\left(\left(P\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)$$
6	5	simplbi	$$⊢\exists r\in A\left(PC\left(P\underset{\dot{}}{\vee }q\right)\wedge \left(P\underset{\dot{}}{\vee }q\right)C\left(\left(P\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\to PC\left(P\underset{\dot{}}{\vee }q\right)$$
7	6	reximi	$$⊢\exists q\in A\exists r\in A\left(PC\left(P\underset{\dot{}}{\vee }q\right)\wedge \left(P\underset{\dot{}}{\vee }q\right)C\left(\left(P\underset{\dot{}}{\vee }q\right)\underset{\dot{}}{\vee }r\right)\right)\to \exists q\in APC\left(P\underset{\dot{}}{\vee }q\right)$$
8	4 7	syl	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\right)\to \exists q\in APC\left(P\underset{\dot{}}{\vee }q\right)$$