chlejb1i

Description: Hilbert lattice ordering in terms of join. (Contributed by NM, 15-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ch0le.1	$⊢ A \in C_{ℋ}$
	chjcl.2	$⊢ B \in C_{ℋ}$
Assertion	chlejb1i	$⊢ A \subseteq B \leftrightarrow A \lor_{ℋ} B = B$

Step	Hyp	Ref	Expression
1		ch0le.1	$⊢ A \in C_{ℋ}$
2		chjcl.2	$⊢ B \in C_{ℋ}$
3		ssid	$⊢ B \subseteq B$
4	1 2 2	chlubii	$⊢ (A \subseteq B \land B \subseteq B) \to A \lor_{ℋ} B \subseteq B$
5	3 4	mpan2	$⊢ A \subseteq B \to A \lor_{ℋ} B \subseteq B$
6	2 1	chub2i	$⊢ B \subseteq A \lor_{ℋ} B$
7	5 6	jctir	$⊢ A \subseteq B \to (A \lor_{ℋ} B \subseteq B \land B \subseteq A \lor_{ℋ} B)$
8		eqss	$⊢ A \lor_{ℋ} B = B \leftrightarrow (A \lor_{ℋ} B \subseteq B \land B \subseteq A \lor_{ℋ} B)$
9	7 8	sylibr	$⊢ A \subseteq B \to A \lor_{ℋ} B = B$
10	1 2	chub1i	$⊢ A \subseteq A \lor_{ℋ} B$
11		eqimss	$⊢ A \lor_{ℋ} B = B \to A \lor_{ℋ} B \subseteq B$
12	10 11	sstrid	$⊢ A \lor_{ℋ} B = B \to A \subseteq B$
13	9 12	impbii	$⊢ A \subseteq B \leftrightarrow A \lor_{ℋ} B = B$

Metamath Proof Explorer