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

Metamath Proof Explorer

Theorem joincl

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

Ref Expression
Hypotheses joincl.b ⊢ B = Base K
joincl.j ⊢ ∨ ˙ = join ⁡ K
joincl.k ⊢ φ → K ∈ V
joincl.x ⊢ φ → X ∈ B
joincl.y ⊢ φ → Y ∈ B
joincl.e ⊢ φ → X Y ∈ dom ⁡ ∨ ˙
Assertion joincl ⊢ φ → X ∨ ˙ Y ∈ B

Proof

Step Hyp Ref Expression
1 joincl.b ⊢ B = Base K
2 joincl.j ⊢ ∨ ˙ = join ⁡ K
3 joincl.k ⊢ φ → K ∈ V
4 joincl.x ⊢ φ → X ∈ B
5 joincl.y ⊢ φ → Y ∈ B
6 joincl.e ⊢ φ → X Y ∈ dom ⁡ ∨ ˙
7 eqid ⊢ lub ⁡ K = lub ⁡ K
8 7 2 3 4 5 joinval ⊢ φ → X ∨ ˙ Y = lub ⁡ K ⁡ X Y
9 7 2 3 4 5 joindef ⊢ φ → X Y ∈ dom ⁡ ∨ ˙ ↔ X Y ∈ dom ⁡ lub ⁡ K
10 6 9 mpbid ⊢ φ → X Y ∈ dom ⁡ lub ⁡ K
11 1 7 3 10 lubcl ⊢ φ → lub ⁡ K ⁡ X Y ∈ B
12 8 11 eqeltrd ⊢ φ → X ∨ ˙ Y ∈ B