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 ∈ V

Proof

Step	Hyp	Ref	Expression
1		ovex	⊢ ( ℋ ↑m ℋ ) ∈ V
2		hmopf	⊢ ( 𝑡 ∈ HrmOp → 𝑡 : ℋ ⟶ ℋ )
3		ax-hilex	⊢ ℋ ∈ V
4	3 3	elmap	⊢ ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↔ 𝑡 : ℋ ⟶ ℋ )
5	2 4	sylibr	⊢ ( 𝑡 ∈ HrmOp → 𝑡 ∈ ( ℋ ↑m ℋ ) )
6	5	ssriv	⊢ HrmOp ⊆ ( ℋ ↑m ℋ )
7	1 6	ssexi	⊢ HrmOp ∈ V