Metamath Proof Explorer


Theorem rpex

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

Ref Expression
Assertion rpex + ∈ V

Proof

Step Hyp Ref Expression
1 eqid ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
2 1 rpmsubg + ∈ ( SubGrp ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) )
3 2 elexi + ∈ V