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 eqtrdi K V dom ˙ = x y | x y dom G