Metamath Proof Explorer

Theorem meetdm2

Description: The meet of any two elements always exists iff all unordered pairs have GLB. (Contributed by Zhi Wang, 25-Sep-2024)

Ref Expression
Hypotheses joindm2.b ⊢ B = Base K
joindm2.k ⊢ φ → K ∈ V
meetdm2.g ⊢ G = glb ⁡ K
meetdm2.m ⊢ ∧ ˙ = meet ⁡ K
Assertion meetdm2 ⊢ φ → dom ⁡ ∧ ˙ = B × B ↔ ∀ x ∈ B ∀ y ∈ B x y ∈ dom ⁡ G

Proof

Step Hyp Ref Expression
1 joindm2.b ⊢ B = Base K
2 joindm2.k ⊢ φ → K ∈ V
3 meetdm2.g ⊢ G = glb ⁡ K
4 meetdm2.m ⊢ ∧ ˙ = meet ⁡ K
5 1 4 2 meetdmss ⊢ φ → dom ⁡ ∧ ˙ ⊆ B × B
6 eqss ⊢ dom ⁡ ∧ ˙ = B × B ↔ dom ⁡ ∧ ˙ ⊆ B × B ∧ B × B ⊆ dom ⁡ ∧ ˙
7 6 baib ⊢ dom ⁡ ∧ ˙ ⊆ B × B → dom ⁡ ∧ ˙ = B × B ↔ B × B ⊆ dom ⁡ ∧ ˙
8 5 7 syl ⊢ φ → dom ⁡ ∧ ˙ = B × B ↔ B × B ⊆ dom ⁡ ∧ ˙
9 relxp ⊢ Rel ⁡ B × B
10 ssrel ⊢ Rel ⁡ B × B → B × B ⊆ dom ⁡ ∧ ˙ ↔ ∀ x ∀ y x y ∈ B × B → x y ∈ dom ⁡ ∧ ˙
11 9 10 mp1i ⊢ φ → B × B ⊆ dom ⁡ ∧ ˙ ↔ ∀ x ∀ y x y ∈ B × B → x y ∈ dom ⁡ ∧ ˙
12 opelxp ⊢ x y ∈ B × B ↔ x ∈ B ∧ y ∈ B
13 12 a1i ⊢ φ → x y ∈ B × B ↔ x ∈ B ∧ y ∈ B
14 vex ⊢ x ∈ V
15 14 a1i ⊢ φ → x ∈ V
16 vex ⊢ y ∈ V
17 16 a1i ⊢ φ → y ∈ V
18 3 4 2 15 17 meetdef ⊢ φ → x y ∈ dom ⁡ ∧ ˙ ↔ x y ∈ dom ⁡ G
19 13 18 imbi12d ⊢ φ → x y ∈ B × B → x y ∈ dom ⁡ ∧ ˙ ↔ x ∈ B ∧ y ∈ B → x y ∈ dom ⁡ G
20 19 2albidv ⊢ φ → ∀ x ∀ y x y ∈ B × B → x y ∈ dom ⁡ ∧ ˙ ↔ ∀ x ∀ y x ∈ B ∧ y ∈ B → x y ∈ dom ⁡ G
21 r2al ⊢ ∀ x ∈ B ∀ y ∈ B x y ∈ dom ⁡ G ↔ ∀ x ∀ y x ∈ B ∧ y ∈ B → x y ∈ dom ⁡ G
22 20 21 bitr4di ⊢ φ → ∀ x ∀ y x y ∈ B × B → x y ∈ dom ⁡ ∧ ˙ ↔ ∀ x ∈ B ∀ y ∈ B x y ∈ dom ⁡ G
23 8 11 22 3bitrd ⊢ φ → dom ⁡ ∧ ˙ = B × B ↔ ∀ x ∈ B ∀ y ∈ B x y ∈ dom ⁡ G