This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem meetcl

Description: Closure of meet of elements in the domain. (Contributed by NM, 12-Sep-2018)

Ref Expression
Hypotheses meetcl.b ⊢ B = Base K
meetcl.m ⊢ ∧ ˙ = meet ⁡ K
meetcl.k ⊢ φ → K ∈ V
meetcl.x ⊢ φ → X ∈ B
meetcl.y ⊢ φ → Y ∈ B
meetcl.e ⊢ φ → X Y ∈ dom ⁡ ∧ ˙
Assertion meetcl ⊢ φ → X ∧ ˙ Y ∈ B

Proof

Step Hyp Ref Expression
1 meetcl.b ⊢ B = Base K
2 meetcl.m ⊢ ∧ ˙ = meet ⁡ K
3 meetcl.k ⊢ φ → K ∈ V
4 meetcl.x ⊢ φ → X ∈ B
5 meetcl.y ⊢ φ → Y ∈ B
6 meetcl.e ⊢ φ → X Y ∈ dom ⁡ ∧ ˙
7 eqid ⊢ glb ⁡ K = glb ⁡ K
8 7 2 3 4 5 meetval ⊢ φ → X ∧ ˙ Y = glb ⁡ K ⁡ X Y
9 7 2 3 4 5 meetdef ⊢ φ → X Y ∈ dom ⁡ ∧ ˙ ↔ X Y ∈ dom ⁡ glb ⁡ K
10 6 9 mpbid ⊢ φ → X Y ∈ dom ⁡ glb ⁡ K
11 1 7 3 10 glbcl ⊢ φ → glb ⁡ K ⁡ X Y ∈ B
12 8 11 eqeltrd ⊢ φ → X ∧ ˙ Y ∈ B