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 = {Base}_{K}$
	joinle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	joinle.j	$⊢ \underset{˙}{\lor} = join (K)$
	joinle.k	$⊢ φ \to K \in Poset$
	joinle.x	$⊢ φ \to X \in B$
	joinle.y	$⊢ φ \to Y \in B$
	joinle.z	$⊢ φ \to Z \in B$
	joinle.e	$⊢ φ \to ⟨X, Y⟩ \in dom \underset{˙}{\lor}$
Assertion	joinle	$⊢ φ \to ((X \underset{˙}{\leq} Z \land Y \underset{˙}{\leq} Z) \leftrightarrow (X \underset{˙}{\lor} Y) \underset{˙}{\leq} Z)$

Proof

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

Metamath Proof Explorer

Theorem joinle

Proof