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	$$⊢\mathrm{HrmOp}\in \mathrm{V}$$

Proof

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