meetdmss

Description: Subset property of domain of meet. (Contributed by NM, 12-Sep-2018)

	Ref	Expression
Hypotheses	meetdmss.b	$⊢ B = {Base}_{K}$
	meetdmss.j	$⊢ \underset{˙}{\land} = meet (K)$
	meetdmss.k	$⊢ φ \to K \in V$
Assertion	meetdmss	$⊢ φ \to dom \underset{˙}{\land} \subseteq B \times B$

Proof

Step	Hyp	Ref	Expression
1		meetdmss.b	$⊢ B = {Base}_{K}$
2		meetdmss.j	$⊢ \underset{˙}{\land} = meet (K)$
3		meetdmss.k	$⊢ φ \to K \in V$
4		relopab	$⊢ Rel \{⟨x, y⟩ \| \{x, y\} \in dom glb (K)\}$
5		eqid	$⊢ glb (K) = glb (K)$
6	5 2	meetdm	$⊢ K \in V \to dom \underset{˙}{\land} = \{⟨x, y⟩ \| \{x, y\} \in dom glb (K)\}$
7	3 6	syl	$⊢ φ \to dom \underset{˙}{\land} = \{⟨x, y⟩ \| \{x, y\} \in dom glb (K)\}$
8	7	releqd	$⊢ φ \to (Rel dom \underset{˙}{\land} \leftrightarrow Rel \{⟨x, y⟩ \| \{x, y\} \in dom glb (K)\})$
9	4 8	mpbiri	$⊢ φ \to Rel dom \underset{˙}{\land}$
10		vex	$⊢ x \in V$
11	10	a1i	$⊢ φ \to x \in V$
12		vex	$⊢ y \in V$
13	12	a1i	$⊢ φ \to y \in V$
14	5 2 3 11 13	meetdef	$⊢ φ \to (⟨x, y⟩ \in dom \underset{˙}{\land} \leftrightarrow \{x, y\} \in dom glb (K))$
15		eqid	$⊢ \leq_{K} = \leq_{K}$
16	3	adantr	$⊢ (φ \land \{x, y\} \in dom glb (K)) \to K \in V$
17		simpr	$⊢ (φ \land \{x, y\} \in dom glb (K)) \to \{x, y\} \in dom glb (K)$
18	1 15 5 16 17	glbelss	$⊢ (φ \land \{x, y\} \in dom glb (K)) \to \{x, y\} \subseteq B$
19	18	ex	$⊢ φ \to (\{x, y\} \in dom glb (K) \to \{x, y\} \subseteq B)$
20	10 12	prss	$⊢ (x \in B \land y \in B) \leftrightarrow \{x, y\} \subseteq B$
21		opelxpi	$⊢ (x \in B \land y \in B) \to ⟨x, y⟩ \in (B \times B)$
22	20 21	sylbir	$⊢ \{x, y\} \subseteq B \to ⟨x, y⟩ \in (B \times B)$
23	19 22	syl6	$⊢ φ \to (\{x, y\} \in dom glb (K) \to ⟨x, y⟩ \in (B \times B))$
24	14 23	sylbid	$⊢ φ \to (⟨x, y⟩ \in dom \underset{˙}{\land} \to ⟨x, y⟩ \in (B \times B))$
25	9 24	relssdv	$⊢ φ \to dom \underset{˙}{\land} \subseteq B \times B$

Metamath Proof Explorer

Theorem meetdmss

Proof