meetval

Description: Meet value. Since both sides evaluate to (/) when they don't exist, for convenience we drop the { X , Y } e. dom G requirement. (Contributed by NM, 9-Sep-2018)

	Ref	Expression
Hypotheses	meetdef.u	$⊢ G = glb (K)$
	meetdef.m	$⊢ \underset{˙}{\land} = meet (K)$
	meetdef.k	$⊢ φ \to K \in V$
	meetdef.x	$⊢ φ \to X \in W$
	meetdef.y	$⊢ φ \to Y \in Z$
Assertion	meetval	$⊢ φ \to X \underset{˙}{\land} Y = G (\{X, Y\})$

Proof

Step	Hyp	Ref	Expression
1		meetdef.u	$⊢ G = glb (K)$
2		meetdef.m	$⊢ \underset{˙}{\land} = meet (K)$
3		meetdef.k	$⊢ φ \to K \in V$
4		meetdef.x	$⊢ φ \to X \in W$
5		meetdef.y	$⊢ φ \to Y \in Z$
6	1 2	meetfval2	$⊢ K \in V \to \underset{˙}{\land} = \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom G \land z = G (\{x, y\}))\}$
7	3 6	syl	$⊢ φ \to \underset{˙}{\land} = \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom G \land z = G (\{x, y\}))\}$
8	7	oveqd	$⊢ φ \to X \underset{˙}{\land} Y = X \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom G \land z = G (\{x, y\}))\} Y$
9	8	adantr	$⊢ (φ \land \{X, Y\} \in dom G) \to X \underset{˙}{\land} Y = X \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom G \land z = G (\{x, y\}))\} Y$
10		simpr	$⊢ (φ \land \{X, Y\} \in dom G) \to \{X, Y\} \in dom G$
11		eqidd	$⊢ (φ \land \{X, Y\} \in dom G) \to G (\{X, Y\}) = G (\{X, Y\})$
12		fvexd	$⊢ φ \to G (\{X, Y\}) \in V$
13		preq12	$⊢ (x = X \land y = Y) \to \{x, y\} = \{X, Y\}$
14	13	eleq1d	$⊢ (x = X \land y = Y) \to (\{x, y\} \in dom G \leftrightarrow \{X, Y\} \in dom G)$
15	14	3adant3	$⊢ (x = X \land y = Y \land z = G (\{X, Y\})) \to (\{x, y\} \in dom G \leftrightarrow \{X, Y\} \in dom G)$
16		simp3	$⊢ (x = X \land y = Y \land z = G (\{X, Y\})) \to z = G (\{X, Y\})$
17	13	fveq2d	$⊢ (x = X \land y = Y) \to G (\{x, y\}) = G (\{X, Y\})$
18	17	3adant3	$⊢ (x = X \land y = Y \land z = G (\{X, Y\})) \to G (\{x, y\}) = G (\{X, Y\})$
19	16 18	eqeq12d	$⊢ (x = X \land y = Y \land z = G (\{X, Y\})) \to (z = G (\{x, y\}) \leftrightarrow G (\{X, Y\}) = G (\{X, Y\}))$
20	15 19	anbi12d	$⊢ (x = X \land y = Y \land z = G (\{X, Y\})) \to ((\{x, y\} \in dom G \land z = G (\{x, y\})) \leftrightarrow (\{X, Y\} \in dom G \land G (\{X, Y\}) = G (\{X, Y\})))$
21		moeq	$⊢ \exists^{*} z z = G (\{x, y\})$
22	21	moani	$⊢ \exists^{*} z (\{x, y\} \in dom G \land z = G (\{x, y\}))$
23		eqid	$⊢ \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom G \land z = G (\{x, y\}))\} = \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom G \land z = G (\{x, y\}))\}$
24	20 22 23	ovigg	$⊢ (X \in W \land Y \in Z \land G (\{X, Y\}) \in V) \to ((\{X, Y\} \in dom G \land G (\{X, Y\}) = G (\{X, Y\})) \to X \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom G \land z = G (\{x, y\}))\} Y = G (\{X, Y\}))$
25	4 5 12 24	syl3anc	$⊢ φ \to ((\{X, Y\} \in dom G \land G (\{X, Y\}) = G (\{X, Y\})) \to X \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom G \land z = G (\{x, y\}))\} Y = G (\{X, Y\}))$
26	25	adantr	$⊢ (φ \land \{X, Y\} \in dom G) \to ((\{X, Y\} \in dom G \land G (\{X, Y\}) = G (\{X, Y\})) \to X \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom G \land z = G (\{x, y\}))\} Y = G (\{X, Y\}))$
27	10 11 26	mp2and	$⊢ (φ \land \{X, Y\} \in dom G) \to X \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom G \land z = G (\{x, y\}))\} Y = G (\{X, Y\})$
28	9 27	eqtrd	$⊢ (φ \land \{X, Y\} \in dom G) \to X \underset{˙}{\land} Y = G (\{X, Y\})$
29	1 2 3 4 5	meetdef	$⊢ φ \to (⟨X, Y⟩ \in dom \underset{˙}{\land} \leftrightarrow \{X, Y\} \in dom G)$
30	29	notbid	$⊢ φ \to (\neg ⟨X, Y⟩ \in dom \underset{˙}{\land} \leftrightarrow \neg \{X, Y\} \in dom G)$
31		df-ov	$⊢ X \underset{˙}{\land} Y = \underset{˙}{\land} (⟨X, Y⟩)$
32		ndmfv	$⊢ \neg ⟨X, Y⟩ \in dom \underset{˙}{\land} \to \underset{˙}{\land} (⟨X, Y⟩) = \emptyset$
33	31 32	syl5eq	$⊢ \neg ⟨X, Y⟩ \in dom \underset{˙}{\land} \to X \underset{˙}{\land} Y = \emptyset$
34	30 33	syl6bir	$⊢ φ \to (\neg \{X, Y\} \in dom G \to X \underset{˙}{\land} Y = \emptyset)$
35	34	imp	$⊢ (φ \land \neg \{X, Y\} \in dom G) \to X \underset{˙}{\land} Y = \emptyset$
36		ndmfv	$⊢ \neg \{X, Y\} \in dom G \to G (\{X, Y\}) = \emptyset$
37	36	adantl	$⊢ (φ \land \neg \{X, Y\} \in dom G) \to G (\{X, Y\}) = \emptyset$
38	35 37	eqtr4d	$⊢ (φ \land \neg \{X, Y\} \in dom G) \to X \underset{˙}{\land} Y = G (\{X, Y\})$
39	28 38	pm2.61dan	$⊢ φ \to X \underset{˙}{\land} Y = G (\{X, Y\})$

Metamath Proof Explorer

Theorem meetval

Proof