latlem

	Ref	Expression
Hypotheses	latlem.b	$⊢ B = {Base}_{K}$
	latlem.j	$⊢ \underset{˙}{\lor} = join (K)$
	latlem.m	$⊢ \underset{˙}{\land} = meet (K)$
Assertion	latlem	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\lor} Y \in B \land X \underset{˙}{\land} Y \in B)$

Proof

Step	Hyp	Ref	Expression
1		latlem.b	$⊢ B = {Base}_{K}$
2		latlem.j	$⊢ \underset{˙}{\lor} = join (K)$
3		latlem.m	$⊢ \underset{˙}{\land} = meet (K)$
4		simp1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to K \in Lat$
5		simp2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \in B$
6		simp3	$⊢ (K \in Lat \land X \in B \land Y \in B) \to Y \in B$
7		opelxpi	$⊢ (X \in B \land Y \in B) \to ⟨X, Y⟩ \in (B \times B)$
8	7	3adant1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ⟨X, Y⟩ \in (B \times B)$
9	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))$
10		simprl	$⊢ (K \in Poset \land (dom \underset{˙}{\lor} = B \times B \land dom \underset{˙}{\land} = B \times B)) \to dom \underset{˙}{\lor} = B \times B$
11	9 10	sylbi	$⊢ K \in Lat \to dom \underset{˙}{\lor} = B \times B$
12	11	3ad2ant1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to dom \underset{˙}{\lor} = B \times B$
13	8 12	eleqtrrd	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ⟨X, Y⟩ \in dom \underset{˙}{\lor}$
14	1 2 4 5 6 13	joincl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y \in B$
15		simprr	$⊢ (K \in Poset \land (dom \underset{˙}{\lor} = B \times B \land dom \underset{˙}{\land} = B \times B)) \to dom \underset{˙}{\land} = B \times B$
16	9 15	sylbi	$⊢ K \in Lat \to dom \underset{˙}{\land} = B \times B$
17	16	3ad2ant1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to dom \underset{˙}{\land} = B \times B$
18	8 17	eleqtrrd	$⊢ (K \in Lat \land X \in B \land Y \in B) \to ⟨X, Y⟩ \in dom \underset{˙}{\land}$
19	1 3 4 5 6 18	meetcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
20	14 19	jca	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\lor} Y \in B \land X \underset{˙}{\land} Y \in B)$

Metamath Proof Explorer

Theorem latlem

Proof