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	$⊢ \underset{˙}{\land} = meet (K)$
Assertion	meetdm	$⊢ K \in V \to dom \underset{˙}{\land} = \{⟨x, y⟩ \| \{x, y\} \in dom G\}$

Step	Hyp	Ref	Expression
1		meetfval.u	$⊢ G = glb (K)$
2		meetfval.m	$⊢ \underset{˙}{\land} = meet (K)$
3	1 2	meetfval2	$⊢ K \in V \to \underset{˙}{\land} = \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom G \land z = G (\{x, y\}))\}$
4	3	dmeqd	$⊢ K \in V \to dom \underset{˙}{\land} = dom \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom G \land z = G (\{x, y\}))\}$
5		dmoprab	$⊢ dom \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom G \land z = G (\{x, y\}))\} = \{⟨x, y⟩ \| \exists z (\{x, y\} \in dom G \land z = G (\{x, y\}))\}$
6		fvex	$⊢ G (\{x, y\}) \in V$
7	6	isseti	$⊢ \exists z z = G (\{x, y\})$
8		19.42v	$⊢ \exists z (\{x, y\} \in dom G \land z = G (\{x, y\})) \leftrightarrow (\{x, y\} \in dom G \land \exists z z = G (\{x, y\}))$
9	7 8	mpbiran2	$⊢ \exists z (\{x, y\} \in dom G \land z = G (\{x, y\})) \leftrightarrow \{x, y\} \in dom G$
10	9	opabbii	$⊢ \{⟨x, y⟩ \| \exists z (\{x, y\} \in dom G \land z = G (\{x, y\}))\} = \{⟨x, y⟩ \| \{x, y\} \in dom G\}$
11	5 10	eqtri	$⊢ dom \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom G \land z = G (\{x, y\}))\} = \{⟨x, y⟩ \| \{x, y\} \in dom G\}$
12	4 11	eqtrdi	$⊢ K \in V \to dom \underset{˙}{\land} = \{⟨x, y⟩ \| \{x, y\} \in dom G\}$

Metamath Proof Explorer