joindmss

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

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

Proof

Step	Hyp	Ref	Expression
1		joindmss.b	$⊢ B = {Base}_{K}$
2		joindmss.j	$⊢ \underset{˙}{\lor} = join (K)$
3		joindmss.k	$⊢ φ \to K \in V$
4		relopab	$⊢ Rel \{⟨x, y⟩ \| \{x, y\} \in dom lub (K)\}$
5		eqid	$⊢ lub (K) = lub (K)$
6	5 2	joindm	$⊢ K \in V \to dom \underset{˙}{\lor} = \{⟨x, y⟩ \| \{x, y\} \in dom lub (K)\}$
7	3 6	syl	$⊢ φ \to dom \underset{˙}{\lor} = \{⟨x, y⟩ \| \{x, y\} \in dom lub (K)\}$
8	7	releqd	$⊢ φ \to (Rel dom \underset{˙}{\lor} \leftrightarrow Rel \{⟨x, y⟩ \| \{x, y\} \in dom lub (K)\})$
9	4 8	mpbiri	$⊢ φ \to Rel dom \underset{˙}{\lor}$
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	joindef	$⊢ φ \to (⟨x, y⟩ \in dom \underset{˙}{\lor} \leftrightarrow \{x, y\} \in dom lub (K))$
15		eqid	$⊢ \leq_{K} = \leq_{K}$
16	3	adantr	$⊢ (φ \land \{x, y\} \in dom lub (K)) \to K \in V$
17		simpr	$⊢ (φ \land \{x, y\} \in dom lub (K)) \to \{x, y\} \in dom lub (K)$
18	1 15 5 16 17	lubelss	$⊢ (φ \land \{x, y\} \in dom lub (K)) \to \{x, y\} \subseteq B$
19	18	ex	$⊢ φ \to (\{x, y\} \in dom lub (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 lub (K) \to ⟨x, y⟩ \in (B \times B))$
24	14 23	sylbid	$⊢ φ \to (⟨x, y⟩ \in dom \underset{˙}{\lor} \to ⟨x, y⟩ \in (B \times B))$
25	9 24	relssdv	$⊢ φ \to dom \underset{˙}{\lor} \subseteq B \times B$

Metamath Proof Explorer

Theorem joindmss

Proof