This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wunom

Description: A weak universe contains all the finite ordinals, and hence is infinite. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypothesis wun0.1 
|- ( ph -> U e. WUni )
Assertion wunom 
|- ( ph -> _om C_ U )

Proof

Step Hyp Ref Expression
1 wun0.1 
 |-  ( ph -> U e. WUni )
2 1 adantr 
 |-  ( ( ph /\ x e. _om ) -> U e. WUni )
3 1 wunr1om 
 |-  ( ph -> ( R1 " _om ) C_ U )
4 r1funlim 
 |-  ( Fun R1 /\ Lim dom R1 )
5 4 simpli 
 |-  Fun R1
6 4 simpri 
 |-  Lim dom R1
7 limomss 
 |-  ( Lim dom R1 -> _om C_ dom R1 )
8 6 7 ax-mp 
 |-  _om C_ dom R1
9 funimass4 
 |-  ( ( Fun R1 /\ _om C_ dom R1 ) -> ( ( R1 " _om ) C_ U <-> A. x e. _om ( R1 ` x ) e. U ) )
10 5 8 9 mp2an 
 |-  ( ( R1 " _om ) C_ U <-> A. x e. _om ( R1 ` x ) e. U )
11 3 10 sylib 
 |-  ( ph -> A. x e. _om ( R1 ` x ) e. U )
12 11 r19.21bi 
 |-  ( ( ph /\ x e. _om ) -> ( R1 ` x ) e. U )
13 simpr 
 |-  ( ( ph /\ x e. _om ) -> x e. _om )
14 8 13 sselid 
 |-  ( ( ph /\ x e. _om ) -> x e. dom R1 )
15 onssr1 
 |-  ( x e. dom R1 -> x C_ ( R1 ` x ) )
16 14 15 syl 
 |-  ( ( ph /\ x e. _om ) -> x C_ ( R1 ` x ) )
17 2 12 16 wunss 
 |-  ( ( ph /\ x e. _om ) -> x e. U )
18 17 ex 
 |-  ( ph -> ( x e. _om -> x e. U ) )
19 18 ssrdv 
 |-  ( ph -> _om C_ U )