Metamath Proof Explorer

Theorem meetdm

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

Ref Expression
Hypotheses meetfval.u ⊢ G = glb ⁡ K
meetfval.m ⊢ ∧ ˙ = meet ⁡ K
Assertion meetdm ⊢ K ∈ V → dom ⁡ ∧ ˙ = x y | x y ∈ dom ⁡ G

Proof

Step Hyp Ref Expression
1 meetfval.u ⊢ G = glb ⁡ K
2 meetfval.m ⊢ ∧ ˙ = meet ⁡ K
3 1 2 meetfval2 ⊢ K ∈ V → ∧ ˙ = x y z | x y ∈ dom ⁡ G ∧ z = G ⁡ x y
4 3 dmeqd ⊢ K ∈ V → dom ⁡ ∧ ˙ = dom ⁡ x y z | x y ∈ dom ⁡ G ∧ z = G ⁡ x y
5 dmoprab ⊢ dom ⁡ x y z | x y ∈ dom ⁡ G ∧ z = G ⁡ x y = x y | ∃ z x y ∈ dom ⁡ G ∧ z = G ⁡ x y
6 fvex ⊢ G ⁡ x y ∈ V
7 6 isseti ⊢ ∃ z z = G ⁡ x y
8 19.42v ⊢ ∃ z x y ∈ dom ⁡ G ∧ z = G ⁡ x y ↔ x y ∈ dom ⁡ G ∧ ∃ z z = G ⁡ x y
9 7 8 mpbiran2 ⊢ ∃ z x y ∈ dom ⁡ G ∧ z = G ⁡ x y ↔ x y ∈ dom ⁡ G
10 9 opabbii ⊢ x y | ∃ z x y ∈ dom ⁡ G ∧ z = G ⁡ x y = x y | x y ∈ dom ⁡ G
11 5 10 eqtri ⊢ dom ⁡ x y z | x y ∈ dom ⁡ G ∧ z = G ⁡ x y = x y | x y ∈ dom ⁡ G
12 4 11 syl6eq ⊢ K ∈ V → dom ⁡ ∧ ˙ = x y | x y ∈ dom ⁡ G