Metamath Proof Explorer

Theorem meetle

Description: A meet 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) (Revised by NM, 12-Sep-2018)

Ref Expression
Hypotheses meetle.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
meetle.l ⊢ ≤ = ( le ‘ 𝐾 )
meetle.m ⊢ ∧ = ( meet ‘ 𝐾 )
meetle.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
meetle.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
meetle.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
meetle.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
meetle.e ⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ )
Assertion meetle ( 𝜑 → ( ( 𝑍 ≤ 𝑋 ∧ 𝑍 ≤ 𝑌 ) ↔ 𝑍 ≤ ( 𝑋 ∧ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 meetle.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 meetle.l ⊢ ≤ = ( le ‘ 𝐾 )
3 meetle.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 meetle.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
5 meetle.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 meetle.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 meetle.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8 meetle.e ⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ )
9 breq1 ⊢ ( 𝑧 = 𝑍 → ( 𝑧 ≤ 𝑋 ↔ 𝑍 ≤ 𝑋 ) )
10 breq1 ⊢ ( 𝑧 = 𝑍 → ( 𝑧 ≤ 𝑌 ↔ 𝑍 ≤ 𝑌 ) )
11 9 10 anbi12d ⊢ ( 𝑧 = 𝑍 → ( ( 𝑧 ≤ 𝑋 ∧ 𝑧 ≤ 𝑌 ) ↔ ( 𝑍 ≤ 𝑋 ∧ 𝑍 ≤ 𝑌 ) ) )
12 breq1 ⊢ ( 𝑧 = 𝑍 → ( 𝑧 ≤ ( 𝑋 ∧ 𝑌 ) ↔ 𝑍 ≤ ( 𝑋 ∧ 𝑌 ) ) )
13 11 12 imbi12d ⊢ ( 𝑧 = 𝑍 → ( ( ( 𝑧 ≤ 𝑋 ∧ 𝑧 ≤ 𝑌 ) → 𝑧 ≤ ( 𝑋 ∧ 𝑌 ) ) ↔ ( ( 𝑍 ≤ 𝑋 ∧ 𝑍 ≤ 𝑌 ) → 𝑍 ≤ ( 𝑋 ∧ 𝑌 ) ) ) )
14 1 2 3 4 5 6 8 meetlem ⊢ ( 𝜑 → ( ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑧 ≤ 𝑋 ∧ 𝑧 ≤ 𝑌 ) → 𝑧 ≤ ( 𝑋 ∧ 𝑌 ) ) ) )
15 14 simprd ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ( ( 𝑧 ≤ 𝑋 ∧ 𝑧 ≤ 𝑌 ) → 𝑧 ≤ ( 𝑋 ∧ 𝑌 ) ) )
16 13 15 7 rspcdva ⊢ ( 𝜑 → ( ( 𝑍 ≤ 𝑋 ∧ 𝑍 ≤ 𝑌 ) → 𝑍 ≤ ( 𝑋 ∧ 𝑌 ) ) )
17 1 2 3 4 5 6 8 lemeet1 ⊢ ( 𝜑 → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )
18 1 3 4 5 6 8 meetcl ⊢ ( 𝜑 → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
19 1 2 postr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑍 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑍 ≤ ( 𝑋 ∧ 𝑌 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 ) → 𝑍 ≤ 𝑋 ) )
20 4 7 18 5 19 syl13anc ⊢ ( 𝜑 → ( ( 𝑍 ≤ ( 𝑋 ∧ 𝑌 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 ) → 𝑍 ≤ 𝑋 ) )
21 17 20 mpan2d ⊢ ( 𝜑 → ( 𝑍 ≤ ( 𝑋 ∧ 𝑌 ) → 𝑍 ≤ 𝑋 ) )
22 1 2 3 4 5 6 8 lemeet2 ⊢ ( 𝜑 → ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 )
23 1 2 postr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑍 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑍 ≤ ( 𝑋 ∧ 𝑌 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 ) → 𝑍 ≤ 𝑌 ) )
24 4 7 18 6 23 syl13anc ⊢ ( 𝜑 → ( ( 𝑍 ≤ ( 𝑋 ∧ 𝑌 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 ) → 𝑍 ≤ 𝑌 ) )
25 22 24 mpan2d ⊢ ( 𝜑 → ( 𝑍 ≤ ( 𝑋 ∧ 𝑌 ) → 𝑍 ≤ 𝑌 ) )
26 21 25 jcad ⊢ ( 𝜑 → ( 𝑍 ≤ ( 𝑋 ∧ 𝑌 ) → ( 𝑍 ≤ 𝑋 ∧ 𝑍 ≤ 𝑌 ) ) )
27 16 26 impbid ⊢ ( 𝜑 → ( ( 𝑍 ≤ 𝑋 ∧ 𝑍 ≤ 𝑌 ) ↔ 𝑍 ≤ ( 𝑋 ∧ 𝑌 ) ) )