Metamath Proof Explorer

Theorem joindef

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

Ref Expression
Hypotheses joindef.u ⊢ U = lub ⁡ K
joindef.j ⊢ ∨ ˙ = join ⁡ K
joindef.k ⊢ φ → K ∈ V
joindef.x ⊢ φ → X ∈ W
joindef.y ⊢ φ → Y ∈ Z
Assertion joindef ⊢ φ → X Y ∈ dom ⁡ ∨ ˙ ↔ X Y ∈ dom ⁡ U

Proof

Step Hyp Ref Expression
1 joindef.u ⊢ U = lub ⁡ K
2 joindef.j ⊢ ∨ ˙ = join ⁡ K
3 joindef.k ⊢ φ → K ∈ V
4 joindef.x ⊢ φ → X ∈ W
5 joindef.y ⊢ φ → Y ∈ Z
6 1 2 joindm ⊢ K ∈ V → dom ⁡ ∨ ˙ = x y | x y ∈ dom ⁡ U
7 6 eleq2d ⊢ K ∈ V → X Y ∈ dom ⁡ ∨ ˙ ↔ X Y ∈ x y | x y ∈ dom ⁡ U
8 3 7 syl ⊢ φ → X Y ∈ dom ⁡ ∨ ˙ ↔ X Y ∈ x y | x y ∈ dom ⁡ U
9 preq1 ⊢ x = X → x y = X y
10 9 eleq1d ⊢ x = X → x y ∈ dom ⁡ U ↔ X y ∈ dom ⁡ U
11 preq2 ⊢ y = Y → X y = X Y
12 11 eleq1d ⊢ y = Y → X y ∈ dom ⁡ U ↔ X Y ∈ dom ⁡ U
13 10 12 opelopabg ⊢ X ∈ W ∧ Y ∈ Z → X Y ∈ x y | x y ∈ dom ⁡ U ↔ X Y ∈ dom ⁡ U
14 4 5 13 syl2anc ⊢ φ → X Y ∈ x y | x y ∈ dom ⁡ U ↔ X Y ∈ dom ⁡ U
15 8 14 bitrd ⊢ φ → X Y ∈ dom ⁡ ∨ ˙ ↔ X Y ∈ dom ⁡ U