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

Metamath Proof Explorer

Theorem hmopex

Description: The class of Hermitian operators is a set. (Contributed by NM, 17-Aug-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	hmopex	$⊢ HrmOp \in V$

Step	Hyp	Ref	Expression
1		ovex	$⊢ ℋ^{ℋ} \in V$
2		hmopf	$⊢ t \in HrmOp \to t : ℋ ⟶ ℋ$
3		ax-hilex	$⊢ ℋ \in V$
4	3 3	elmap	$⊢ t \in (ℋ^{ℋ}) \leftrightarrow t : ℋ ⟶ ℋ$
5	2 4	sylibr	$⊢ t \in HrmOp \to t \in (ℋ^{ℋ})$
6	5	ssriv	$⊢ HrmOp \subseteq ℋ^{ℋ}$
7	1 6	ssexi	$⊢ HrmOp \in V$