meetfval

Description: Value of meet function for a poset. (Contributed by NM, 12-Sep-2011) (Revised by NM, 9-Sep-2018) TODO: prove meetfval2 first to reduce net proof size (existence part)?

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

Proof

Step	Hyp	Ref	Expression
1		meetfval.u	$⊢ G = glb (K)$
2		meetfval.m	$⊢ \underset{˙}{\land} = meet (K)$
3		elex	$⊢ K \in V \to K \in V$
4		fvex	$⊢ {Base}_{K} \in V$
5		moeq	$⊢ \exists^{*} z z = G (\{x, y\})$
6	5	a1i	$⊢ (x \in {Base}_{K} \land y \in {Base}_{K}) \to \exists^{*} z z = G (\{x, y\})$
7		eqid	$⊢ \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = G (\{x, y\}))\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = G (\{x, y\}))\}$
8	4 4 6 7	oprabex	$⊢ \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = G (\{x, y\}))\} \in V$
9	8	a1i	$⊢ K \in V \to \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = G (\{x, y\}))\} \in V$
10	1	glbfun	$⊢ Fun G$
11		funbrfv2b	$⊢ Fun G \to (\{x, y\} G z \leftrightarrow (\{x, y\} \in dom G \land G (\{x, y\}) = z))$
12	10 11	ax-mp	$⊢ \{x, y\} G z \leftrightarrow (\{x, y\} \in dom G \land G (\{x, y\}) = z)$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14		eqid	$⊢ \leq_{K} = \leq_{K}$
15		simpl	$⊢ (K \in V \land \{x, y\} \in dom G) \to K \in V$
16		simpr	$⊢ (K \in V \land \{x, y\} \in dom G) \to \{x, y\} \in dom G$
17	13 14 1 15 16	glbelss	$⊢ (K \in V \land \{x, y\} \in dom G) \to \{x, y\} \subseteq {Base}_{K}$
18	17	ex	$⊢ K \in V \to (\{x, y\} \in dom G \to \{x, y\} \subseteq {Base}_{K})$
19		vex	$⊢ x \in V$
20		vex	$⊢ y \in V$
21	19 20	prss	$⊢ (x \in {Base}_{K} \land y \in {Base}_{K}) \leftrightarrow \{x, y\} \subseteq {Base}_{K}$
22	18 21	imbitrrdi	$⊢ K \in V \to (\{x, y\} \in dom G \to (x \in {Base}_{K} \land y \in {Base}_{K}))$
23		eqcom	$⊢ G (\{x, y\}) = z \leftrightarrow z = G (\{x, y\})$
24	23	biimpi	$⊢ G (\{x, y\}) = z \to z = G (\{x, y\})$
25	22 24	anim12d1	$⊢ K \in V \to ((\{x, y\} \in dom G \land G (\{x, y\}) = z) \to ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = G (\{x, y\})))$
26	12 25	biimtrid	$⊢ K \in V \to (\{x, y\} G z \to ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = G (\{x, y\})))$
27	26	alrimiv	$⊢ K \in V \to \forall z (\{x, y\} G z \to ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = G (\{x, y\})))$
28	27	alrimiv	$⊢ K \in V \to \forall y \forall z (\{x, y\} G z \to ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = G (\{x, y\})))$
29	28	alrimiv	$⊢ K \in V \to \forall x \forall y \forall z (\{x, y\} G z \to ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = G (\{x, y\})))$
30		ssoprab2	$⊢ \forall x \forall y \forall z (\{x, y\} G z \to ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = G (\{x, y\}))) \to \{⟨⟨x, y⟩, z⟩ \| \{x, y\} G z\} \subseteq \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = G (\{x, y\}))\}$
31	29 30	syl	$⊢ K \in V \to \{⟨⟨x, y⟩, z⟩ \| \{x, y\} G z\} \subseteq \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{K} \land y \in {Base}_{K}) \land z = G (\{x, y\}))\}$
32	9 31	ssexd	$⊢ K \in V \to \{⟨⟨x, y⟩, z⟩ \| \{x, y\} G z\} \in V$
33		fveq2	$⊢ p = K \to glb (p) = glb (K)$
34	33 1	eqtr4di	$⊢ p = K \to glb (p) = G$
35	34	breqd	$⊢ p = K \to (\{x, y\} glb (p) z \leftrightarrow \{x, y\} G z)$
36	35	oprabbidv	$⊢ p = K \to \{⟨⟨x, y⟩, z⟩ \| \{x, y\} glb (p) z\} = \{⟨⟨x, y⟩, z⟩ \| \{x, y\} G z\}$
37		df-meet	$⊢ meet = (p \in V ⟼ \{⟨⟨x, y⟩, z⟩ \| \{x, y\} glb (p) z\})$
38	36 37	fvmptg	$⊢ (K \in V \land \{⟨⟨x, y⟩, z⟩ \| \{x, y\} G z\} \in V) \to meet (K) = \{⟨⟨x, y⟩, z⟩ \| \{x, y\} G z\}$
39	32 38	mpdan	$⊢ K \in V \to meet (K) = \{⟨⟨x, y⟩, z⟩ \| \{x, y\} G z\}$
40	2 39	eqtrid	$⊢ K \in V \to \underset{˙}{\land} = \{⟨⟨x, y⟩, z⟩ \| \{x, y\} G z\}$
41	3 40	syl	$⊢ K \in V \to \underset{˙}{\land} = \{⟨⟨x, y⟩, z⟩ \| \{x, y\} G z\}$

Metamath Proof Explorer

Theorem meetfval

Proof