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

Metamath Proof Explorer

Theorem hlrel

Description: The class of all complex Hilbert spaces is a relation. (Contributed by NM, 17-Mar-2007) (New usage is discouraged.)

		Ref	Expression
	Assertion	hlrel	$⊢ Rel {CHil}_{OLD}$

Step	Hyp	Ref	Expression
1		hlobn	$⊢ x \in {CHil}_{OLD} \to x \in CBan$
2	1	ssriv	$⊢ {CHil}_{OLD} \subseteq CBan$
3		bnrel	$⊢ Rel CBan$
4		relss	$⊢ {CHil}_{OLD} \subseteq CBan \to (Rel CBan \to Rel {CHil}_{OLD})$
5	2 3 4	mp2	$⊢ Rel {CHil}_{OLD}$