meetdef

Description: Two ways to say that a meet is defined. (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	meetdef	$⊢ φ \to (⟨X, Y⟩ \in dom \underset{˙}{\land} \leftrightarrow \{X, Y\} \in dom G)$

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	meetdm	$⊢ K \in V \to dom \underset{˙}{\land} = \{⟨x, y⟩ \| \{x, y\} \in dom G\}$
7	6	eleq2d	$⊢ K \in V \to (⟨X, Y⟩ \in dom \underset{˙}{\land} \leftrightarrow ⟨X, Y⟩ \in \{⟨x, y⟩ \| \{x, y\} \in dom G\})$
8	3 7	syl	$⊢ φ \to (⟨X, Y⟩ \in dom \underset{˙}{\land} \leftrightarrow ⟨X, Y⟩ \in \{⟨x, y⟩ \| \{x, y\} \in dom G\})$
9		preq1	$⊢ x = X \to \{x, y\} = \{X, y\}$
10	9	eleq1d	$⊢ x = X \to (\{x, y\} \in dom G \leftrightarrow \{X, y\} \in dom G)$
11		preq2	$⊢ y = Y \to \{X, y\} = \{X, Y\}$
12	11	eleq1d	$⊢ y = Y \to (\{X, y\} \in dom G \leftrightarrow \{X, Y\} \in dom G)$
13	10 12	opelopabg	$⊢ (X \in W \land Y \in Z) \to (⟨X, Y⟩ \in \{⟨x, y⟩ \| \{x, y\} \in dom G\} \leftrightarrow \{X, Y\} \in dom G)$
14	4 5 13	syl2anc	$⊢ φ \to (⟨X, Y⟩ \in \{⟨x, y⟩ \| \{x, y\} \in dom G\} \leftrightarrow \{X, Y\} \in dom G)$
15	8 14	bitrd	$⊢ φ \to (⟨X, Y⟩ \in dom \underset{˙}{\land} \leftrightarrow \{X, Y\} \in dom G)$

Metamath Proof Explorer