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

Metamath Proof Explorer

Theorem wunr1om

Description: A weak universe is infinite, because it contains all the finite levels of the cumulative hierarchy. (Contributed by Mario Carneiro, 2-Jan-2017)

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

Proof

Step Hyp Ref Expression
1 wun0.1 
 |-  ( ph -> U e. WUni )
2 fveq2 
 |-  ( x = (/) -> ( R1 ` x ) = ( R1 ` (/) ) )
3 2 eleq1d 
 |-  ( x = (/) -> ( ( R1 ` x ) e. U <-> ( R1 ` (/) ) e. U ) )
4 fveq2 
 |-  ( x = y -> ( R1 ` x ) = ( R1 ` y ) )
5 4 eleq1d 
 |-  ( x = y -> ( ( R1 ` x ) e. U <-> ( R1 ` y ) e. U ) )
6 fveq2 
 |-  ( x = suc y -> ( R1 ` x ) = ( R1 ` suc y ) )
7 6 eleq1d 
 |-  ( x = suc y -> ( ( R1 ` x ) e. U <-> ( R1 ` suc y ) e. U ) )
8 r10 
 |-  ( R1 ` (/) ) = (/)
9 1 wun0 
 |-  ( ph -> (/) e. U )
10 8 9 eqeltrid 
 |-  ( ph -> ( R1 ` (/) ) e. U )
11 1 adantr 
 |-  ( ( ph /\ ( R1 ` y ) e. U ) -> U e. WUni )
12 simpr 
 |-  ( ( ph /\ ( R1 ` y ) e. U ) -> ( R1 ` y ) e. U )
13 11 12 wunpw 
 |-  ( ( ph /\ ( R1 ` y ) e. U ) -> ~P ( R1 ` y ) e. U )
14 nnon 
 |-  ( y e. _om -> y e. On )
15 r1suc 
 |-  ( y e. On -> ( R1 ` suc y ) = ~P ( R1 ` y ) )
16 14 15 syl 
 |-  ( y e. _om -> ( R1 ` suc y ) = ~P ( R1 ` y ) )
17 16 eleq1d 
 |-  ( y e. _om -> ( ( R1 ` suc y ) e. U <-> ~P ( R1 ` y ) e. U ) )
18 13 17 imbitrrid 
 |-  ( y e. _om -> ( ( ph /\ ( R1 ` y ) e. U ) -> ( R1 ` suc y ) e. U ) )
19 18 expd 
 |-  ( y e. _om -> ( ph -> ( ( R1 ` y ) e. U -> ( R1 ` suc y ) e. U ) ) )
20 3 5 7 10 19 finds2 
 |-  ( x e. _om -> ( ph -> ( R1 ` x ) e. U ) )
21 eleq1 
 |-  ( ( R1 ` x ) = y -> ( ( R1 ` x ) e. U <-> y e. U ) )
22 21 imbi2d 
 |-  ( ( R1 ` x ) = y -> ( ( ph -> ( R1 ` x ) e. U ) <-> ( ph -> y e. U ) ) )
23 20 22 syl5ibcom 
 |-  ( x e. _om -> ( ( R1 ` x ) = y -> ( ph -> y e. U ) ) )
24 23 rexlimiv 
 |-  ( E. x e. _om ( R1 ` x ) = y -> ( ph -> y e. U ) )
25 r1fnon 
 |-  R1 Fn On
26 fnfun 
 |-  ( R1 Fn On -> Fun R1 )
27 25 26 ax-mp 
 |-  Fun R1
28 fvelima 
 |-  ( ( Fun R1 /\ y e. ( R1 " _om ) ) -> E. x e. _om ( R1 ` x ) = y )
29 27 28 mpan 
 |-  ( y e. ( R1 " _om ) -> E. x e. _om ( R1 ` x ) = y )
30 24 29 syl11 
 |-  ( ph -> ( y e. ( R1 " _om ) -> y e. U ) )
31 30 ssrdv 
 |-  ( ph -> ( R1 " _om ) C_ U )