Metamath Proof Explorer

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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
joinle.l ⊢ ≤ = ( le ‘ 𝐾 )
joinle.j ⊢ ∨ = ( join ‘ 𝐾 )
joinle.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
joinle.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
joinle.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
joinle.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
joinle.e ⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∨ )
Assertion joinle ( 𝜑 → ( ( 𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍 ) ↔ ( 𝑋 ∨ 𝑌 ) ≤ 𝑍 ) )

Proof

Step Hyp Ref Expression
1 joinle.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 joinle.l ⊢ ≤ = ( le ‘ 𝐾 )
3 joinle.j ⊢ ∨ = ( join ‘ 𝐾 )
4 joinle.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
5 joinle.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 joinle.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 joinle.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8 joinle.e ⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∨ )
9 breq2 ⊢ ( 𝑧 = 𝑍 → ( 𝑋 ≤ 𝑧 ↔ 𝑋 ≤ 𝑍 ) )
10 breq2 ⊢ ( 𝑧 = 𝑍 → ( 𝑌 ≤ 𝑧 ↔ 𝑌 ≤ 𝑍 ) )
11 9 10 anbi12d ⊢ ( 𝑧 = 𝑍 → ( ( 𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧 ) ↔ ( 𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍 ) ) )
12 breq2 ⊢ ( 𝑧 = 𝑍 → ( ( 𝑋 ∨ 𝑌 ) ≤ 𝑧 ↔ ( 𝑋 ∨ 𝑌 ) ≤ 𝑍 ) )
13 11 12 imbi12d ⊢ ( 𝑧 = 𝑍 → ( ( ( 𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧 ) → ( 𝑋 ∨ 𝑌 ) ≤ 𝑧 ) ↔ ( ( 𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍 ) → ( 𝑋 ∨ 𝑌 ) ≤ 𝑍 ) ) )
14 1 2 3 4 5 6 8 joinlem ⊢ ( 𝜑 → ( ( 𝑋 ≤ ( 𝑋 ∨ 𝑌 ) ∧ 𝑌 ≤ ( 𝑋 ∨ 𝑌 ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧 ) → ( 𝑋 ∨ 𝑌 ) ≤ 𝑧 ) ) )
15 14 simprd ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ( ( 𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧 ) → ( 𝑋 ∨ 𝑌 ) ≤ 𝑧 ) )
16 13 15 7 rspcdva ⊢ ( 𝜑 → ( ( 𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍 ) → ( 𝑋 ∨ 𝑌 ) ≤ 𝑍 ) )
17 1 2 3 4 5 6 8 lejoin1 ⊢ ( 𝜑 → 𝑋 ≤ ( 𝑋 ∨ 𝑌 ) )
18 1 3 4 5 6 8 joincl ⊢ ( 𝜑 → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
19 1 2 postr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ 𝑌 ) ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) )
20 4 5 18 7 19 syl13anc ⊢ ( 𝜑 → ( ( 𝑋 ≤ ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ 𝑌 ) ≤ 𝑍 ) → 𝑋 ≤ 𝑍 ) )
21 17 20 mpand ⊢ ( 𝜑 → ( ( 𝑋 ∨ 𝑌 ) ≤ 𝑍 → 𝑋 ≤ 𝑍 ) )
22 1 2 3 4 5 6 8 lejoin2 ⊢ ( 𝜑 → 𝑌 ≤ ( 𝑋 ∨ 𝑌 ) )
23 1 2 postr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑌 ≤ ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ 𝑌 ) ≤ 𝑍 ) → 𝑌 ≤ 𝑍 ) )
24 4 6 18 7 23 syl13anc ⊢ ( 𝜑 → ( ( 𝑌 ≤ ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑋 ∨ 𝑌 ) ≤ 𝑍 ) → 𝑌 ≤ 𝑍 ) )
25 22 24 mpand ⊢ ( 𝜑 → ( ( 𝑋 ∨ 𝑌 ) ≤ 𝑍 → 𝑌 ≤ 𝑍 ) )
26 21 25 jcad ⊢ ( 𝜑 → ( ( 𝑋 ∨ 𝑌 ) ≤ 𝑍 → ( 𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍 ) ) )
27 16 26 impbid ⊢ ( 𝜑 → ( ( 𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍 ) ↔ ( 𝑋 ∨ 𝑌 ) ≤ 𝑍 ) )