Metamath Proof Explorer

Theorem rpex

Description: The positive reals form a set. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Assertion rpex 
|- RR+ e. _V

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
2 1 rpmsubg 
 |-  RR+ e. ( SubGrp ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) )
3 2 elexi 
 |-  RR+ e. _V