Metamath Proof Explorer

Theorem joindm

Description: Domain of join function for a poset-type structure. (Contributed by NM, 16-Sep-2018)

Ref Expression
Hypotheses joinfval.u ⊢ U = lub ⁡ K
joinfval.j ⊢ ∨ ˙ = join ⁡ K
Assertion joindm ⊢ K ∈ V → dom ⁡ ∨ ˙ = x y | x y ∈ dom ⁡ U

Proof

Step Hyp Ref Expression
1 joinfval.u ⊢ U = lub ⁡ K
2 joinfval.j ⊢ ∨ ˙ = join ⁡ K
3 1 2 joinfval2 ⊢ K ∈ V → ∨ ˙ = x y z | x y ∈ dom ⁡ U ∧ z = U ⁡ x y
4 3 dmeqd ⊢ K ∈ V → dom ⁡ ∨ ˙ = dom ⁡ x y z | x y ∈ dom ⁡ U ∧ z = U ⁡ x y
5 dmoprab ⊢ dom ⁡ x y z | x y ∈ dom ⁡ U ∧ z = U ⁡ x y = x y | ∃ z x y ∈ dom ⁡ U ∧ z = U ⁡ x y
6 fvex ⊢ U ⁡ x y ∈ V
7 6 isseti ⊢ ∃ z z = U ⁡ x y
8 19.42v ⊢ ∃ z x y ∈ dom ⁡ U ∧ z = U ⁡ x y ↔ x y ∈ dom ⁡ U ∧ ∃ z z = U ⁡ x y
9 7 8 mpbiran2 ⊢ ∃ z x y ∈ dom ⁡ U ∧ z = U ⁡ x y ↔ x y ∈ dom ⁡ U
10 9 opabbii ⊢ x y | ∃ z x y ∈ dom ⁡ U ∧ z = U ⁡ x y = x y | x y ∈ dom ⁡ U
11 5 10 eqtri ⊢ dom ⁡ x y z | x y ∈ dom ⁡ U ∧ z = U ⁡ x y = x y | x y ∈ dom ⁡ U
12 4 11 eqtrdi ⊢ K ∈ V → dom ⁡ ∨ ˙ = x y | x y ∈ dom ⁡ U