Theorem joinle

Description: A join is less than or equal to a third value iff each argument is less than or equal to the third value. (Contributed by NM, 16-Sep-2011)

	Ref	Expression
Hypotheses	joinle.b	$$⊢B={\mathrm{Base}}_K$$
	joinle.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	joinle.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	joinle.k	$$⊢\phi \to K\in \mathrm{Poset}$$
	joinle.x	$$⊢\phi \to X\in B$$
	joinle.y	$$⊢\phi \to Y\in B$$
	joinle.z	$$⊢\phi \to Z\in B$$
	joinle.e	$$⊢\phi \to ⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\vee }$$
Assertion	joinle	$$⊢\phi \to \left(\left(X\underset{\dot{}}{\le }Z\wedge Y\underset{\dot{}}{\le }Z\right)\leftrightarrow \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }Z\right)$$

Proof

Step	Hyp	Ref	Expression
1		joinle.b	$$⊢B={\mathrm{Base}}_K$$
2		joinle.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		joinle.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		joinle.k	$$⊢\phi \to K\in \mathrm{Poset}$$
5		joinle.x	$$⊢\phi \to X\in B$$
6		joinle.y	$$⊢\phi \to Y\in B$$
7		joinle.z	$$⊢\phi \to Z\in B$$
8		joinle.e	$$⊢\phi \to ⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\vee }$$
9		breq2	$$⊢z=Z\to \left(X\underset{\dot{}}{\le }z\leftrightarrow X\underset{\dot{}}{\le }Z\right)$$
10		breq2	$$⊢z=Z\to \left(Y\underset{\dot{}}{\le }z\leftrightarrow Y\underset{\dot{}}{\le }Z\right)$$
11	9 10	anbi12d	$$⊢z=Z\to \left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\leftrightarrow \left(X\underset{\dot{}}{\le }Z\wedge Y\underset{\dot{}}{\le }Z\right)\right)$$
12		breq2	$$⊢z=Z\to \left(\left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }z\leftrightarrow \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }Z\right)$$
13	11 12	imbi12d	$$⊢z=Z\to \left(\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }z\right)\leftrightarrow \left(\left(X\underset{\dot{}}{\le }Z\wedge Y\underset{\dot{}}{\le }Z\right)\to \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }Z\right)\right)$$
14	1 2 3 4 5 6 8	joinlem	$$⊢\phi \to \left(\left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\wedge Y\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\right)\wedge \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }z\right)\right)$$
15	14	simprd	$$⊢\phi \to \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }z\right)$$
16	13 15 7	rspcdva	$$⊢\phi \to \left(\left(X\underset{\dot{}}{\le }Z\wedge Y\underset{\dot{}}{\le }Z\right)\to \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }Z\right)$$
17	1 2 3 4 5 6 8	lejoin1	$$⊢\phi \to X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)$$
18	1 3 4 5 6 8	joincl	$$⊢\phi \to X\underset{\dot{}}{\vee }Y\in B$$
19	1 2	postr	$$⊢\left(K\in \mathrm{Poset}\wedge \left(X\in B\wedge X\underset{\dot{}}{\vee }Y\in B\wedge Z\in B\right)\right)\to \left(\left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\wedge \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }Z\right)\to X\underset{\dot{}}{\le }Z\right)$$
20	4 5 18 7 19	syl13anc	$$⊢\phi \to \left(\left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\wedge \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }Z\right)\to X\underset{\dot{}}{\le }Z\right)$$
21	17 20	mpand	$$⊢\phi \to \left(\left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }Z\to X\underset{\dot{}}{\le }Z\right)$$
22	1 2 3 4 5 6 8	lejoin2	$$⊢\phi \to Y\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)$$
23	1 2	postr	$$⊢\left(K\in \mathrm{Poset}\wedge \left(Y\in B\wedge X\underset{\dot{}}{\vee }Y\in B\wedge Z\in B\right)\right)\to \left(\left(Y\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\wedge \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }Z\right)\to Y\underset{\dot{}}{\le }Z\right)$$
24	4 6 18 7 23	syl13anc	$$⊢\phi \to \left(\left(Y\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\wedge \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }Z\right)\to Y\underset{\dot{}}{\le }Z\right)$$
25	22 24	mpand	$$⊢\phi \to \left(\left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }Z\to Y\underset{\dot{}}{\le }Z\right)$$
26	21 25	jcad	$$⊢\phi \to \left(\left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }Z\to \left(X\underset{\dot{}}{\le }Z\wedge Y\underset{\dot{}}{\le }Z\right)\right)$$
27	16 26	impbid	$$⊢\phi \to \left(\left(X\underset{\dot{}}{\le }Z\wedge Y\underset{\dot{}}{\le }Z\right)\leftrightarrow \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }Z\right)$$