Metamath Proof Explorer

Theorem r1wunlim

Description: The weak universes in the cumulative hierarchy are exactly the limit ordinals. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion r1wunlim 
|- ( A e. V -> ( ( R1 ` A ) e. WUni <-> Lim A ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( A e. V /\ ( R1 ` A ) e. WUni ) -> ( R1 ` A ) e. WUni )
2 1 wun0 
 |-  ( ( A e. V /\ ( R1 ` A ) e. WUni ) -> (/) e. ( R1 ` A ) )
3 elfvdm 
 |-  ( (/) e. ( R1 ` A ) -> A e. dom R1 )
4 2 3 syl 
 |-  ( ( A e. V /\ ( R1 ` A ) e. WUni ) -> A e. dom R1 )
5 r1fnon 
 |-  R1 Fn On
6 5 fndmi 
 |-  dom R1 = On
7 4 6 eleqtrdi 
 |-  ( ( A e. V /\ ( R1 ` A ) e. WUni ) -> A e. On )
8 eloni 
 |-  ( A e. On -> Ord A )
9 7 8 syl 
 |-  ( ( A e. V /\ ( R1 ` A ) e. WUni ) -> Ord A )
10 n0i 
 |-  ( (/) e. ( R1 ` A ) -> -. ( R1 ` A ) = (/) )
11 2 10 syl 
 |-  ( ( A e. V /\ ( R1 ` A ) e. WUni ) -> -. ( R1 ` A ) = (/) )
12 fveq2 
 |-  ( A = (/) -> ( R1 ` A ) = ( R1 ` (/) ) )
13 r10 
 |-  ( R1 ` (/) ) = (/)
14 12 13 eqtrdi 
 |-  ( A = (/) -> ( R1 ` A ) = (/) )
15 11 14 nsyl 
 |-  ( ( A e. V /\ ( R1 ` A ) e. WUni ) -> -. A = (/) )
16 suceloni 
 |-  ( A e. On -> suc A e. On )
17 7 16 syl 
 |-  ( ( A e. V /\ ( R1 ` A ) e. WUni ) -> suc A e. On )
18 sucidg 
 |-  ( A e. On -> A e. suc A )
19 7 18 syl 
 |-  ( ( A e. V /\ ( R1 ` A ) e. WUni ) -> A e. suc A )
20 r1ord 
 |-  ( suc A e. On -> ( A e. suc A -> ( R1 ` A ) e. ( R1 ` suc A ) ) )
21 17 19 20 sylc 
 |-  ( ( A e. V /\ ( R1 ` A ) e. WUni ) -> ( R1 ` A ) e. ( R1 ` suc A ) )
22 r1elwf 
 |-  ( ( R1 ` A ) e. ( R1 ` suc A ) -> ( R1 ` A ) e. U. ( R1 " On ) )
23 wfelirr 
 |-  ( ( R1 ` A ) e. U. ( R1 " On ) -> -. ( R1 ` A ) e. ( R1 ` A ) )
24 21 22 23 3syl 
 |-  ( ( A e. V /\ ( R1 ` A ) e. WUni ) -> -. ( R1 ` A ) e. ( R1 ` A ) )
25 simprr 
 |-  ( ( ( A e. V /\ ( R1 ` A ) e. WUni ) /\ ( x e. On /\ A = suc x ) ) -> A = suc x )
26 25 fveq2d 
 |-  ( ( ( A e. V /\ ( R1 ` A ) e. WUni ) /\ ( x e. On /\ A = suc x ) ) -> ( R1 ` A ) = ( R1 ` suc x ) )
27 r1suc 
 |-  ( x e. On -> ( R1 ` suc x ) = ~P ( R1 ` x ) )
28 27 ad2antrl 
 |-  ( ( ( A e. V /\ ( R1 ` A ) e. WUni ) /\ ( x e. On /\ A = suc x ) ) -> ( R1 ` suc x ) = ~P ( R1 ` x ) )
29 26 28 eqtrd 
 |-  ( ( ( A e. V /\ ( R1 ` A ) e. WUni ) /\ ( x e. On /\ A = suc x ) ) -> ( R1 ` A ) = ~P ( R1 ` x ) )
30 simplr 
 |-  ( ( ( A e. V /\ ( R1 ` A ) e. WUni ) /\ ( x e. On /\ A = suc x ) ) -> ( R1 ` A ) e. WUni )
31 7 adantr 
 |-  ( ( ( A e. V /\ ( R1 ` A ) e. WUni ) /\ ( x e. On /\ A = suc x ) ) -> A e. On )
32 sucidg 
 |-  ( x e. On -> x e. suc x )
33 32 ad2antrl 
 |-  ( ( ( A e. V /\ ( R1 ` A ) e. WUni ) /\ ( x e. On /\ A = suc x ) ) -> x e. suc x )
34 33 25 eleqtrrd 
 |-  ( ( ( A e. V /\ ( R1 ` A ) e. WUni ) /\ ( x e. On /\ A = suc x ) ) -> x e. A )
35 r1ord 
 |-  ( A e. On -> ( x e. A -> ( R1 ` x ) e. ( R1 ` A ) ) )
36 31 34 35 sylc 
 |-  ( ( ( A e. V /\ ( R1 ` A ) e. WUni ) /\ ( x e. On /\ A = suc x ) ) -> ( R1 ` x ) e. ( R1 ` A ) )
37 30 36 wunpw 
 |-  ( ( ( A e. V /\ ( R1 ` A ) e. WUni ) /\ ( x e. On /\ A = suc x ) ) -> ~P ( R1 ` x ) e. ( R1 ` A ) )
38 29 37 eqeltrd 
 |-  ( ( ( A e. V /\ ( R1 ` A ) e. WUni ) /\ ( x e. On /\ A = suc x ) ) -> ( R1 ` A ) e. ( R1 ` A ) )
39 38 rexlimdvaa 
 |-  ( ( A e. V /\ ( R1 ` A ) e. WUni ) -> ( E. x e. On A = suc x -> ( R1 ` A ) e. ( R1 ` A ) ) )
40 24 39 mtod 
 |-  ( ( A e. V /\ ( R1 ` A ) e. WUni ) -> -. E. x e. On A = suc x )
41 ioran 
 |-  ( -. ( A = (/) \/ E. x e. On A = suc x ) <-> ( -. A = (/) /\ -. E. x e. On A = suc x ) )
42 15 40 41 sylanbrc 
 |-  ( ( A e. V /\ ( R1 ` A ) e. WUni ) -> -. ( A = (/) \/ E. x e. On A = suc x ) )
43 dflim3 
 |-  ( Lim A <-> ( Ord A /\ -. ( A = (/) \/ E. x e. On A = suc x ) ) )
44 9 42 43 sylanbrc 
 |-  ( ( A e. V /\ ( R1 ` A ) e. WUni ) -> Lim A )
45 r1limwun 
 |-  ( ( A e. V /\ Lim A ) -> ( R1 ` A ) e. WUni )
46 44 45 impbida 
 |-  ( A e. V -> ( ( R1 ` A ) e. WUni <-> Lim A ) )