Metamath Proof Explorer

Theorem pnfex

Description: Plus infinity exists. (Contributed by David A. Wheeler, 8-Dec-2018) (Revised by Steven Nguyen, 7-Dec-2022)

Ref Expression
Assertion pnfex 
|- +oo e. _V

Proof

Step Hyp Ref Expression
1 df-pnf 
 |-  +oo = ~P U. CC
2 cnex 
 |-  CC e. _V
3 2 uniex 
 |-  U. CC e. _V
4 3 pwex 
 |-  ~P U. CC e. _V
5 1 4 eqeltri 
 |-  +oo e. _V