Theorem 4atex2-0bOLDN

Description: Same as 4atex2 except that T is zero. (Contributed by NM, 27-May-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	4that.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	4that.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	4that.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	4that.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
Assertion	4atex2-0bOLDN	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge T=\mathrm{0.}\left(K\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge S\underset{\dot{}}{\vee }z=T\underset{\dot{}}{\vee }z\right)$$

Proof

Step	Hyp	Ref	Expression
1		4that.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		4that.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		4that.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		4that.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
5		simp1	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge T=\mathrm{0.}\left(K\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
6		simp21	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge T=\mathrm{0.}\left(K\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)$$
7		simp22	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge T=\mathrm{0.}\left(K\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)$$
8		simp32	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge T=\mathrm{0.}\left(K\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to T=\mathrm{0.}\left(K\right)$$
9		simp31	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge T=\mathrm{0.}\left(K\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to P\ne Q$$
10		simp23	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge T=\mathrm{0.}\left(K\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)$$
11		simp33	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge T=\mathrm{0.}\left(K\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)$$
12	1 2 3 4	4atex2-0aOLDN	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge T=\mathrm{0.}\left(K\right)\right)\wedge \left(P\ne Q\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)$$
13	5 6 7 8 9 10 11 12	syl133anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge T=\mathrm{0.}\left(K\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)$$
14		eqcom	$$⊢S\underset{\dot{}}{\vee }z=T\underset{\dot{}}{\vee }z\leftrightarrow T\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z$$
15	14	anbi2i	$$⊢\left(\neg z\underset{\dot{}}{\le }W\wedge S\underset{\dot{}}{\vee }z=T\underset{\dot{}}{\vee }z\right)\leftrightarrow \left(\neg z\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)$$
16	15	rexbii	$$⊢\exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge S\underset{\dot{}}{\vee }z=T\underset{\dot{}}{\vee }z\right)\leftrightarrow \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\vee }z=S\underset{\dot{}}{\vee }z\right)$$
17	13 16	sylibr	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\wedge \left(S\in A\wedge \neg S\underset{\dot{}}{\le }W\right)\right)\wedge \left(P\ne Q\wedge T=\mathrm{0.}\left(K\right)\wedge \exists r\in A\left(\neg r\underset{\dot{}}{\le }W\wedge P\underset{\dot{}}{\vee }r=Q\underset{\dot{}}{\vee }r\right)\right)\right)\to \exists z\in A\left(\neg z\underset{\dot{}}{\le }W\wedge S\underset{\dot{}}{\vee }z=T\underset{\dot{}}{\vee }z\right)$$