Description: The positive reals form a set. (Contributed by Glauco Siliprandi, 11-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | rpex | ⊢ ℝ+ ∈ V |
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 |