Metamath Proof Explorer

Theorem meetdef

Description: Two ways to say that a meet is defined. (Contributed by NM, 9-Sep-2018)

Ref Expression
Hypotheses meetdef.u ⊢ G = glb ⁡ K
meetdef.m ⊢ ∧ ˙ = meet ⁡ K
meetdef.k ⊢ φ → K ∈ V
meetdef.x ⊢ φ → X ∈ W
meetdef.y ⊢ φ → Y ∈ Z
Assertion meetdef ⊢ φ → X Y ∈ dom ⁡ ∧ ˙ ↔ X Y ∈ dom ⁡ G

Proof

Step Hyp Ref Expression
1 meetdef.u ⊢ G = glb ⁡ K
2 meetdef.m ⊢ ∧ ˙ = meet ⁡ K
3 meetdef.k ⊢ φ → K ∈ V
4 meetdef.x ⊢ φ → X ∈ W
5 meetdef.y ⊢ φ → Y ∈ Z
6 1 2 meetdm ⊢ K ∈ V → dom ⁡ ∧ ˙ = x y | x y ∈ dom ⁡ G
7 6 eleq2d ⊢ K ∈ V → X Y ∈ dom ⁡ ∧ ˙ ↔ X Y ∈ x y | x y ∈ dom ⁡ G
8 3 7 syl ⊢ φ → X Y ∈ dom ⁡ ∧ ˙ ↔ X Y ∈ x y | x y ∈ dom ⁡ G
9 preq1 ⊢ x = X → x y = X y
10 9 eleq1d ⊢ x = X → x y ∈ dom ⁡ G ↔ X y ∈ dom ⁡ G
11 preq2 ⊢ y = Y → X y = X Y
12 11 eleq1d ⊢ y = Y → X y ∈ dom ⁡ G ↔ X Y ∈ dom ⁡ G
13 10 12 opelopabg ⊢ X ∈ W ∧ Y ∈ Z → X Y ∈ x y | x y ∈ dom ⁡ G ↔ X Y ∈ dom ⁡ G
14 4 5 13 syl2anc ⊢ φ → X Y ∈ x y | x y ∈ dom ⁡ G ↔ X Y ∈ dom ⁡ G
15 8 14 bitrd ⊢ φ → X Y ∈ dom ⁡ ∧ ˙ ↔ X Y ∈ dom ⁡ G