Theorem paddasslem6

Description: Lemma for paddass . (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	paddasslem6	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(p\in A\wedge s\in A\right)\wedge z\in A\right)\wedge \left(s\ne z\wedge s\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }z\right)\right)\right)\to p\underset{\dot{}}{\le }\left(s\underset{\dot{}}{\vee }z\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		simpl1	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(p\in A\wedge s\in A\right)\wedge z\in A\right)\wedge \left(s\ne z\wedge s\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }z\right)\right)\right)\to K\in \mathrm{HL}$$
5		simpl2r	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(p\in A\wedge s\in A\right)\wedge z\in A\right)\wedge \left(s\ne z\wedge s\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }z\right)\right)\right)\to s\in A$$
6		simpl2l	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(p\in A\wedge s\in A\right)\wedge z\in A\right)\wedge \left(s\ne z\wedge s\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }z\right)\right)\right)\to p\in A$$
7		simpl3	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(p\in A\wedge s\in A\right)\wedge z\in A\right)\wedge \left(s\ne z\wedge s\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }z\right)\right)\right)\to z\in A$$
8	5 6 7	3jca	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(p\in A\wedge s\in A\right)\wedge z\in A\right)\wedge \left(s\ne z\wedge s\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }z\right)\right)\right)\to \left(s\in A\wedge p\in A\wedge z\in A\right)$$
9		simprl	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(p\in A\wedge s\in A\right)\wedge z\in A\right)\wedge \left(s\ne z\wedge s\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }z\right)\right)\right)\to s\ne z$$
10	4 8 9	3jca	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(p\in A\wedge s\in A\right)\wedge z\in A\right)\wedge \left(s\ne z\wedge s\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }z\right)\right)\right)\to \left(K\in \mathrm{HL}\wedge \left(s\in A\wedge p\in A\wedge z\in A\right)\wedge s\ne z\right)$$
11		simprr	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(p\in A\wedge s\in A\right)\wedge z\in A\right)\wedge \left(s\ne z\wedge s\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }z\right)\right)\right)\to s\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }z\right)$$
12	1 2 3	hlatexch2	$$⊢\left(K\in \mathrm{HL}\wedge \left(s\in A\wedge p\in A\wedge z\in A\right)\wedge s\ne z\right)\to \left(s\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }z\right)\to p\underset{\dot{}}{\le }\left(s\underset{\dot{}}{\vee }z\right)\right)$$
13	10 11 12	sylc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(p\in A\wedge s\in A\right)\wedge z\in A\right)\wedge \left(s\ne z\wedge s\underset{\dot{}}{\le }\left(p\underset{\dot{}}{\vee }z\right)\right)\right)\to p\underset{\dot{}}{\le }\left(s\underset{\dot{}}{\vee }z\right)$$