meetfval2

Description: Value of meet function for a poset. (Contributed by NM, 12-Sep-2011) (Revised by NM, 9-Sep-2018)

	Ref	Expression
Hypotheses	meetfval.u	$⊢ G = glb (K)$
	meetfval.m	$⊢ \underset{˙}{\land} = meet (K)$
Assertion	meetfval2	$⊢ K \in V \to \underset{˙}{\land} = \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom G \land z = G (\{x, y\}))\}$

Step	Hyp	Ref	Expression
1		meetfval.u	$⊢ G = glb (K)$
2		meetfval.m	$⊢ \underset{˙}{\land} = meet (K)$
3	1 2	meetfval	$⊢ K \in V \to \underset{˙}{\land} = \{⟨⟨x, y⟩, z⟩ \| \{x, y\} G z\}$
4	1	glbfun	$⊢ Fun G$
5		funbrfv2b	$⊢ Fun G \to (\{x, y\} G z \leftrightarrow (\{x, y\} \in dom G \land G (\{x, y\}) = z))$
6	4 5	ax-mp	$⊢ \{x, y\} G z \leftrightarrow (\{x, y\} \in dom G \land G (\{x, y\}) = z)$
7		eqcom	$⊢ G (\{x, y\}) = z \leftrightarrow z = G (\{x, y\})$
8	7	anbi2i	$⊢ (\{x, y\} \in dom G \land G (\{x, y\}) = z) \leftrightarrow (\{x, y\} \in dom G \land z = G (\{x, y\}))$
9	6 8	bitri	$⊢ \{x, y\} G z \leftrightarrow (\{x, y\} \in dom G \land z = G (\{x, y\}))$
10	9	oprabbii	$⊢ \{⟨⟨x, y⟩, z⟩ \| \{x, y\} G z\} = \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom G \land z = G (\{x, y\}))\}$
11	3 10	eqtrdi	$⊢ K \in V \to \underset{˙}{\land} = \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom G \land z = G (\{x, y\}))\}$

Metamath Proof Explorer