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

Metamath Proof Explorer

Theorem chm0i

Description: Meet with Hilbert lattice zero. (Contributed by NM, 6-Aug-2004) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	ch0le.1	$⊢ A \in C_{ℋ}$
	Assertion	chm0i	$⊢ A \cap 0_{ℋ} = 0_{ℋ}$

Step	Hyp	Ref	Expression
1		ch0le.1	$⊢ A \in C_{ℋ}$
2		inss2	$⊢ A \cap 0_{ℋ} \subseteq 0_{ℋ}$
3	1	ch0lei	$⊢ 0_{ℋ} \subseteq A$
4		ssid	$⊢ 0_{ℋ} \subseteq 0_{ℋ}$
5	3 4	ssini	$⊢ 0_{ℋ} \subseteq A \cap 0_{ℋ}$
6	2 5	eqssi	$⊢ A \cap 0_{ℋ} = 0_{ℋ}$