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 e. _V

Proof

Step Hyp Ref Expression
1 ovex 
 |-  ( ~H ^m ~H ) e. _V
2 hmopf 
 |-  ( t e. HrmOp -> t : ~H --> ~H )
3 ax-hilex 
 |-  ~H e. _V
4 3 3 elmap 
 |-  ( t e. ( ~H ^m ~H ) <-> t : ~H --> ~H )
5 2 4 sylibr 
 |-  ( t e. HrmOp -> t e. ( ~H ^m ~H ) )
6 5 ssriv 
 |-  HrmOp C_ ( ~H ^m ~H )
7 1 6 ssexi 
 |-  HrmOp e. _V