Metamath Proof Explorer

Theorem r1limwun

Description: Each limit stage in the cumulative hierarchy is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion r1limwun 
|- ( ( A e. V /\ Lim A ) -> ( R1 ` A ) e. WUni )

Proof

Step Hyp Ref Expression
1 r1tr 
 |-  Tr ( R1 ` A )
2 1 a1i 
 |-  ( ( A e. V /\ Lim A ) -> Tr ( R1 ` A ) )
3 limelon 
 |-  ( ( A e. V /\ Lim A ) -> A e. On )
4 r1fnon 
 |-  R1 Fn On
5 4 fndmi 
 |-  dom R1 = On
6 3 5 eleqtrrdi 
 |-  ( ( A e. V /\ Lim A ) -> A e. dom R1 )
7 onssr1 
 |-  ( A e. dom R1 -> A C_ ( R1 ` A ) )
8 6 7 syl 
 |-  ( ( A e. V /\ Lim A ) -> A C_ ( R1 ` A ) )
9 0ellim 
 |-  ( Lim A -> (/) e. A )
10 9 adantl 
 |-  ( ( A e. V /\ Lim A ) -> (/) e. A )
11 8 10 sseldd 
 |-  ( ( A e. V /\ Lim A ) -> (/) e. ( R1 ` A ) )
12 11 ne0d 
 |-  ( ( A e. V /\ Lim A ) -> ( R1 ` A ) =/= (/) )
13 rankuni 
 |-  ( rank ` U. x ) = U. ( rank ` x )
14 rankon 
 |-  ( rank ` x ) e. On
15 eloni 
 |-  ( ( rank ` x ) e. On -> Ord ( rank ` x ) )
16 orduniss 
 |-  ( Ord ( rank ` x ) -> U. ( rank ` x ) C_ ( rank ` x ) )
17 14 15 16 mp2b 
 |-  U. ( rank ` x ) C_ ( rank ` x )
18 17 a1i 
 |-  ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) -> U. ( rank ` x ) C_ ( rank ` x ) )
19 rankr1ai 
 |-  ( x e. ( R1 ` A ) -> ( rank ` x ) e. A )
20 19 adantl 
 |-  ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) -> ( rank ` x ) e. A )
21 onuni 
 |-  ( ( rank ` x ) e. On -> U. ( rank ` x ) e. On )
22 14 21 ax-mp 
 |-  U. ( rank ` x ) e. On
23 3 adantr 
 |-  ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) -> A e. On )
24 ontr2 
 |-  ( ( U. ( rank ` x ) e. On /\ A e. On ) -> ( ( U. ( rank ` x ) C_ ( rank ` x ) /\ ( rank ` x ) e. A ) -> U. ( rank ` x ) e. A ) )
25 22 23 24 sylancr 
 |-  ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) -> ( ( U. ( rank ` x ) C_ ( rank ` x ) /\ ( rank ` x ) e. A ) -> U. ( rank ` x ) e. A ) )
26 18 20 25 mp2and 
 |-  ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) -> U. ( rank ` x ) e. A )
27 13 26 eqeltrid 
 |-  ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) -> ( rank ` U. x ) e. A )
28 r1elwf 
 |-  ( x e. ( R1 ` A ) -> x e. U. ( R1 " On ) )
29 28 adantl 
 |-  ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) -> x e. U. ( R1 " On ) )
30 uniwf 
 |-  ( x e. U. ( R1 " On ) <-> U. x e. U. ( R1 " On ) )
31 29 30 sylib 
 |-  ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) -> U. x e. U. ( R1 " On ) )
32 6 adantr 
 |-  ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) -> A e. dom R1 )
33 rankr1ag 
 |-  ( ( U. x e. U. ( R1 " On ) /\ A e. dom R1 ) -> ( U. x e. ( R1 ` A ) <-> ( rank ` U. x ) e. A ) )
34 31 32 33 syl2anc 
 |-  ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) -> ( U. x e. ( R1 ` A ) <-> ( rank ` U. x ) e. A ) )
35 27 34 mpbird 
 |-  ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) -> U. x e. ( R1 ` A ) )
36 r1pwcl 
 |-  ( Lim A -> ( x e. ( R1 ` A ) <-> ~P x e. ( R1 ` A ) ) )
37 36 adantl 
 |-  ( ( A e. V /\ Lim A ) -> ( x e. ( R1 ` A ) <-> ~P x e. ( R1 ` A ) ) )
38 37 biimpa 
 |-  ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) -> ~P x e. ( R1 ` A ) )
39 28 ad2antlr 
 |-  ( ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) /\ y e. ( R1 ` A ) ) -> x e. U. ( R1 " On ) )
40 r1elwf 
 |-  ( y e. ( R1 ` A ) -> y e. U. ( R1 " On ) )
41 40 adantl 
 |-  ( ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) /\ y e. ( R1 ` A ) ) -> y e. U. ( R1 " On ) )
42 rankprb 
 |-  ( ( x e. U. ( R1 " On ) /\ y e. U. ( R1 " On ) ) -> ( rank ` { x , y } ) = suc ( ( rank ` x ) u. ( rank ` y ) ) )
43 39 41 42 syl2anc 
 |-  ( ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) /\ y e. ( R1 ` A ) ) -> ( rank ` { x , y } ) = suc ( ( rank ` x ) u. ( rank ` y ) ) )
44 limord 
 |-  ( Lim A -> Ord A )
45 44 ad3antlr 
 |-  ( ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) /\ y e. ( R1 ` A ) ) -> Ord A )
46 20 adantr 
 |-  ( ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) /\ y e. ( R1 ` A ) ) -> ( rank ` x ) e. A )
47 rankr1ai 
 |-  ( y e. ( R1 ` A ) -> ( rank ` y ) e. A )
48 47 adantl 
 |-  ( ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) /\ y e. ( R1 ` A ) ) -> ( rank ` y ) e. A )
49 ordunel 
 |-  ( ( Ord A /\ ( rank ` x ) e. A /\ ( rank ` y ) e. A ) -> ( ( rank ` x ) u. ( rank ` y ) ) e. A )
50 45 46 48 49 syl3anc 
 |-  ( ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) /\ y e. ( R1 ` A ) ) -> ( ( rank ` x ) u. ( rank ` y ) ) e. A )
51 limsuc 
 |-  ( Lim A -> ( ( ( rank ` x ) u. ( rank ` y ) ) e. A <-> suc ( ( rank ` x ) u. ( rank ` y ) ) e. A ) )
52 51 ad3antlr 
 |-  ( ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) /\ y e. ( R1 ` A ) ) -> ( ( ( rank ` x ) u. ( rank ` y ) ) e. A <-> suc ( ( rank ` x ) u. ( rank ` y ) ) e. A ) )
53 50 52 mpbid 
 |-  ( ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) /\ y e. ( R1 ` A ) ) -> suc ( ( rank ` x ) u. ( rank ` y ) ) e. A )
54 43 53 eqeltrd 
 |-  ( ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) /\ y e. ( R1 ` A ) ) -> ( rank ` { x , y } ) e. A )
55 prwf 
 |-  ( ( x e. U. ( R1 " On ) /\ y e. U. ( R1 " On ) ) -> { x , y } e. U. ( R1 " On ) )
56 39 41 55 syl2anc 
 |-  ( ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) /\ y e. ( R1 ` A ) ) -> { x , y } e. U. ( R1 " On ) )
57 32 adantr 
 |-  ( ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) /\ y e. ( R1 ` A ) ) -> A e. dom R1 )
58 rankr1ag 
 |-  ( ( { x , y } e. U. ( R1 " On ) /\ A e. dom R1 ) -> ( { x , y } e. ( R1 ` A ) <-> ( rank ` { x , y } ) e. A ) )
59 56 57 58 syl2anc 
 |-  ( ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) /\ y e. ( R1 ` A ) ) -> ( { x , y } e. ( R1 ` A ) <-> ( rank ` { x , y } ) e. A ) )
60 54 59 mpbird 
 |-  ( ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) /\ y e. ( R1 ` A ) ) -> { x , y } e. ( R1 ` A ) )
61 60 ralrimiva 
 |-  ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) -> A. y e. ( R1 ` A ) { x , y } e. ( R1 ` A ) )
62 35 38 61 3jca 
 |-  ( ( ( A e. V /\ Lim A ) /\ x e. ( R1 ` A ) ) -> ( U. x e. ( R1 ` A ) /\ ~P x e. ( R1 ` A ) /\ A. y e. ( R1 ` A ) { x , y } e. ( R1 ` A ) ) )
63 62 ralrimiva 
 |-  ( ( A e. V /\ Lim A ) -> A. x e. ( R1 ` A ) ( U. x e. ( R1 ` A ) /\ ~P x e. ( R1 ` A ) /\ A. y e. ( R1 ` A ) { x , y } e. ( R1 ` A ) ) )
64 fvex 
 |-  ( R1 ` A ) e. _V
65 iswun 
 |-  ( ( R1 ` A ) e. _V -> ( ( R1 ` A ) e. WUni <-> ( Tr ( R1 ` A ) /\ ( R1 ` A ) =/= (/) /\ A. x e. ( R1 ` A ) ( U. x e. ( R1 ` A ) /\ ~P x e. ( R1 ` A ) /\ A. y e. ( R1 ` A ) { x , y } e. ( R1 ` A ) ) ) ) )
66 64 65 ax-mp 
 |-  ( ( R1 ` A ) e. WUni <-> ( Tr ( R1 ` A ) /\ ( R1 ` A ) =/= (/) /\ A. x e. ( R1 ` A ) ( U. x e. ( R1 ` A ) /\ ~P x e. ( R1 ` A ) /\ A. y e. ( R1 ` A ) { x , y } e. ( R1 ` A ) ) ) )
67 2 12 63 66 syl3anbrc 
 |-  ( ( A e. V /\ Lim A ) -> ( R1 ` A ) e. WUni )