Metamath Proof Explorer

Theorem joindm2

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

Ref Expression
Hypotheses joindm2.b ⊢ B = Base K
joindm2.k ⊢ φ → K ∈ V
joindm2.u ⊢ U = lub ⁡ K
joindm2.j ⊢ ∨ ˙ = join ⁡ K
Assertion joindm2 ⊢ φ → dom ⁡ ∨ ˙ = B × B ↔ ∀ x ∈ B ∀ y ∈ B x y ∈ dom ⁡ U

Proof

Step Hyp Ref Expression
1 joindm2.b ⊢ B = Base K
2 joindm2.k ⊢ φ → K ∈ V
3 joindm2.u ⊢ U = lub ⁡ K
4 joindm2.j ⊢ ∨ ˙ = join ⁡ K
5 1 4 2 joindmss ⊢ φ → 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 joindef ⊢ φ → x y ∈ dom ⁡ ∨ ˙ ↔ x y ∈ dom ⁡ U
19 13 18 imbi12d ⊢ φ → x y ∈ B × B → x y ∈ dom ⁡ ∨ ˙ ↔ x ∈ B ∧ y ∈ B → x y ∈ dom ⁡ U
20 19 2albidv ⊢ φ → ∀ x ∀ y x y ∈ B × B → x y ∈ dom ⁡ ∨ ˙ ↔ ∀ x ∀ y x ∈ B ∧ y ∈ B → x y ∈ dom ⁡ U
21 r2al ⊢ ∀ x ∈ B ∀ y ∈ B x y ∈ dom ⁡ U ↔ ∀ x ∀ y x ∈ B ∧ y ∈ B → x y ∈ dom ⁡ U
22 20 21 bitr4di ⊢ φ → ∀ x ∀ y x y ∈ B × B → x y ∈ dom ⁡ ∨ ˙ ↔ ∀ x ∈ B ∀ y ∈ B x y ∈ dom ⁡ U
23 8 11 22 3bitrd ⊢ φ → dom ⁡ ∨ ˙ = B × B ↔ ∀ x ∈ B ∀ y ∈ B x y ∈ dom ⁡ U