Metamath Proof Explorer

Theorem wunex3

Description: Construct a weak universe from a given set. This version of wunex has a simpler proof, but requires the axiom of regularity. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypothesis wunex3.u 
|- U = ( R1 ` ( ( rank ` A ) +o _om ) )
Assertion wunex3 
|- ( A e. V -> ( U e. WUni /\ A C_ U ) )

Proof

Step Hyp Ref Expression
1 wunex3.u 
 |-  U = ( R1 ` ( ( rank ` A ) +o _om ) )
2 r1rankid 
 |-  ( A e. V -> A C_ ( R1 ` ( rank ` A ) ) )
3 rankon 
 |-  ( rank ` A ) e. On
4 omelon 
 |-  _om e. On
5 oacl 
 |-  ( ( ( rank ` A ) e. On /\ _om e. On ) -> ( ( rank ` A ) +o _om ) e. On )
6 3 4 5 mp2an 
 |-  ( ( rank ` A ) +o _om ) e. On
7 peano1 
 |-  (/) e. _om
8 oaord1 
 |-  ( ( ( rank ` A ) e. On /\ _om e. On ) -> ( (/) e. _om <-> ( rank ` A ) e. ( ( rank ` A ) +o _om ) ) )
9 3 4 8 mp2an 
 |-  ( (/) e. _om <-> ( rank ` A ) e. ( ( rank ` A ) +o _om ) )
10 7 9 mpbi 
 |-  ( rank ` A ) e. ( ( rank ` A ) +o _om )
11 r1ord2 
 |-  ( ( ( rank ` A ) +o _om ) e. On -> ( ( rank ` A ) e. ( ( rank ` A ) +o _om ) -> ( R1 ` ( rank ` A ) ) C_ ( R1 ` ( ( rank ` A ) +o _om ) ) ) )
12 6 10 11 mp2 
 |-  ( R1 ` ( rank ` A ) ) C_ ( R1 ` ( ( rank ` A ) +o _om ) )
13 12 1 sseqtrri 
 |-  ( R1 ` ( rank ` A ) ) C_ U
14 2 13 sstrdi 
 |-  ( A e. V -> A C_ U )
15 limom 
 |-  Lim _om
16 4 15 pm3.2i 
 |-  ( _om e. On /\ Lim _om )
17 oalimcl 
 |-  ( ( ( rank ` A ) e. On /\ ( _om e. On /\ Lim _om ) ) -> Lim ( ( rank ` A ) +o _om ) )
18 3 16 17 mp2an 
 |-  Lim ( ( rank ` A ) +o _om )
19 r1limwun 
 |-  ( ( ( ( rank ` A ) +o _om ) e. On /\ Lim ( ( rank ` A ) +o _om ) ) -> ( R1 ` ( ( rank ` A ) +o _om ) ) e. WUni )
20 6 18 19 mp2an 
 |-  ( R1 ` ( ( rank ` A ) +o _om ) ) e. WUni
21 1 20 eqeltri 
 |-  U e. WUni
22 14 21 jctil 
 |-  ( A e. V -> ( U e. WUni /\ A C_ U ) )