Theorem paddasslem3

Description: Lemma for paddass . Restate projective space axiom ps-2 . (Contributed by NM, 8-Jan-2012)

	Ref	Expression
Hypotheses	paddasslem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	paddasslem.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	paddasslem.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	paddasslem3	$$⊢\left(K\in \mathrm{HL}\wedge \left(x\in A\wedge r\in A\wedge y\in A\right)\wedge \left(p\in A\wedge z\in A\right)\right)\to \left(\left(\left(\neg x\underset{\dot{}}{\le }\left(r\underset{\dot{}}{\vee }y\right)\wedge p\ne z\right)\wedge \left(p\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }r\right)\wedge z\underset{\dot{}}{\le }\left(r\underset{\dot{}}{\vee }y\right)\right)\right)\to \exists s\in A\left(s\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\wedge s\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }z\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		paddasslem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		paddasslem.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		paddasslem.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4	1 2 3	ps-2	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(x\in A\wedge r\in A\wedge y\in A\right)\wedge \left(p\in A\wedge z\in A\right)\right)\wedge \left(\left(\neg x\underset{\dot{}}{\le }\left(r\underset{\dot{}}{\vee }y\right)\wedge p\ne z\right)\wedge \left(p\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }r\right)\wedge z\underset{\dot{}}{\le }\left(r\underset{\dot{}}{\vee }y\right)\right)\right)\right)\to \exists s\in A\left(s\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\wedge s\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }z\right)\right)$$
5	4	ex	$$⊢\left(K\in \mathrm{HL}\wedge \left(x\in A\wedge r\in A\wedge y\in A\right)\wedge \left(p\in A\wedge z\in A\right)\right)\to \left(\left(\left(\neg x\underset{\dot{}}{\le }\left(r\underset{\dot{}}{\vee }y\right)\wedge p\ne z\right)\wedge \left(p\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }r\right)\wedge z\underset{\dot{}}{\le }\left(r\underset{\dot{}}{\vee }y\right)\right)\right)\to \exists s\in A\left(s\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\wedge s\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }z\right)\right)\right)$$