latcl2

Description: The join and meet of any two elements exist. (Contributed by NM, 14-Sep-2018)

	Ref	Expression
Hypotheses	latcl2.b	$⊢ B = {Base}_{K}$
	latcl2.j	$⊢ \underset{˙}{\lor} = join (K)$
	latcl2.m	$⊢ \underset{˙}{\land} = meet (K)$
	latcl2.k	$⊢ φ \to K \in Lat$
	latcl2.x	$⊢ φ \to X \in B$
	latcl2.y	$⊢ φ \to Y \in B$
Assertion	latcl2	$⊢ φ \to (⟨X, Y⟩ \in dom \underset{˙}{\lor} \land ⟨X, Y⟩ \in dom \underset{˙}{\land})$

Step	Hyp	Ref	Expression
1		latcl2.b	$⊢ B = {Base}_{K}$
2		latcl2.j	$⊢ \underset{˙}{\lor} = join (K)$
3		latcl2.m	$⊢ \underset{˙}{\land} = meet (K)$
4		latcl2.k	$⊢ φ \to K \in Lat$
5		latcl2.x	$⊢ φ \to X \in B$
6		latcl2.y	$⊢ φ \to Y \in B$
7	5 6	opelxpd	$⊢ φ \to ⟨X, Y⟩ \in (B \times B)$
8	1 2 3	islat	$⊢ K \in Lat \leftrightarrow (K \in Poset \land (dom \underset{˙}{\lor} = B \times B \land dom \underset{˙}{\land} = B \times B))$
9	4 8	sylib	$⊢ φ \to (K \in Poset \land (dom \underset{˙}{\lor} = B \times B \land dom \underset{˙}{\land} = B \times B))$
10	9	simprld	$⊢ φ \to dom \underset{˙}{\lor} = B \times B$
11	7 10	eleqtrrd	$⊢ φ \to ⟨X, Y⟩ \in dom \underset{˙}{\lor}$
12	9	simprrd	$⊢ φ \to dom \underset{˙}{\land} = B \times B$
13	7 12	eleqtrrd	$⊢ φ \to ⟨X, Y⟩ \in dom \underset{˙}{\land}$
14	11 13	jca	$⊢ φ \to (⟨X, Y⟩ \in dom \underset{˙}{\lor} \land ⟨X, Y⟩ \in dom \underset{˙}{\land})$

Metamath Proof Explorer