This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hlatjcl

Description: Closure of join operation. Frequently-used special case of latjcl for atoms. (Contributed by NM, 15-Jun-2012)

	Ref	Expression
Hypotheses	hlatjcl.b	$⊢ B = {Base}_{K}$
	hlatjcl.j	$⊢ \underset{˙}{\lor} = join (K)$
	hlatjcl.a	$⊢ A = Atoms (K)$
Assertion	hlatjcl	$⊢ (K \in HL \land X \in A \land Y \in A) \to X \underset{˙}{\lor} Y \in B$

Step	Hyp	Ref	Expression
1		hlatjcl.b	$⊢ B = {Base}_{K}$
2		hlatjcl.j	$⊢ \underset{˙}{\lor} = join (K)$
3		hlatjcl.a	$⊢ A = Atoms (K)$
4		hllat	$⊢ K \in HL \to K \in Lat$
5	1 3	atbase	$⊢ X \in A \to X \in B$
6	1 3	atbase	$⊢ Y \in A \to Y \in B$
7	1 2	latjcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y \in B$
8	4 5 6 7	syl3an	$⊢ (K \in HL \land X \in A \land Y \in A) \to X \underset{˙}{\lor} Y \in B$