Metamath Proof Explorer

Theorem grur1cld

Description: Grothendieck universes are closed under the cumulative hierarchy function. (Contributed by Rohan Ridenour, 8-Aug-2023)

Ref Expression
Hypotheses grur1cld.1 
|- ( ph -> G e. Univ )
grur1cld.2 
|- ( ph -> A e. G )
Assertion grur1cld 
|- ( ph -> ( R1 ` A ) e. G )

Proof

Step Hyp Ref Expression
1 grur1cld.1 
 |-  ( ph -> G e. Univ )
2 grur1cld.2 
 |-  ( ph -> A e. G )
3 2 adantr 
 |-  ( ( ph /\ A e. On ) -> A e. G )
4 eleq1 
 |-  ( x = (/) -> ( x e. G <-> (/) e. G ) )
5 fveq2 
 |-  ( x = (/) -> ( R1 ` x ) = ( R1 ` (/) ) )
6 5 eleq1d 
 |-  ( x = (/) -> ( ( R1 ` x ) e. G <-> ( R1 ` (/) ) e. G ) )
7 4 6 imbi12d 
 |-  ( x = (/) -> ( ( x e. G -> ( R1 ` x ) e. G ) <-> ( (/) e. G -> ( R1 ` (/) ) e. G ) ) )
8 eleq1 
 |-  ( x = y -> ( x e. G <-> y e. G ) )
9 fveq2 
 |-  ( x = y -> ( R1 ` x ) = ( R1 ` y ) )
10 9 eleq1d 
 |-  ( x = y -> ( ( R1 ` x ) e. G <-> ( R1 ` y ) e. G ) )
11 8 10 imbi12d 
 |-  ( x = y -> ( ( x e. G -> ( R1 ` x ) e. G ) <-> ( y e. G -> ( R1 ` y ) e. G ) ) )
12 eleq1 
 |-  ( x = suc y -> ( x e. G <-> suc y e. G ) )
13 fveq2 
 |-  ( x = suc y -> ( R1 ` x ) = ( R1 ` suc y ) )
14 13 eleq1d 
 |-  ( x = suc y -> ( ( R1 ` x ) e. G <-> ( R1 ` suc y ) e. G ) )
15 12 14 imbi12d 
 |-  ( x = suc y -> ( ( x e. G -> ( R1 ` x ) e. G ) <-> ( suc y e. G -> ( R1 ` suc y ) e. G ) ) )
16 eleq1 
 |-  ( x = A -> ( x e. G <-> A e. G ) )
17 fveq2 
 |-  ( x = A -> ( R1 ` x ) = ( R1 ` A ) )
18 17 eleq1d 
 |-  ( x = A -> ( ( R1 ` x ) e. G <-> ( R1 ` A ) e. G ) )
19 16 18 imbi12d 
 |-  ( x = A -> ( ( x e. G -> ( R1 ` x ) e. G ) <-> ( A e. G -> ( R1 ` A ) e. G ) ) )
20 r10 
 |-  ( R1 ` (/) ) = (/)
21 1 2 gru0eld 
 |-  ( ph -> (/) e. G )
22 20 21 eqeltrid 
 |-  ( ph -> ( R1 ` (/) ) e. G )
23 22 adantr 
 |-  ( ( ph /\ A e. On ) -> ( R1 ` (/) ) e. G )
24 23 a1d 
 |-  ( ( ph /\ A e. On ) -> ( (/) e. G -> ( R1 ` (/) ) e. G ) )
25 simpl1 
 |-  ( ( ( ( ph /\ A e. On ) /\ y e. On /\ ( y e. G -> ( R1 ` y ) e. G ) ) /\ suc y e. G ) -> ( ph /\ A e. On ) )
26 simpl2 
 |-  ( ( ( ( ph /\ A e. On ) /\ y e. On /\ ( y e. G -> ( R1 ` y ) e. G ) ) /\ suc y e. G ) -> y e. On )
27 1 adantr 
 |-  ( ( ph /\ A e. On ) -> G e. Univ )
28 25 27 syl 
 |-  ( ( ( ( ph /\ A e. On ) /\ y e. On /\ ( y e. G -> ( R1 ` y ) e. G ) ) /\ suc y e. G ) -> G e. Univ )
29 simpr 
 |-  ( ( ( ( ph /\ A e. On ) /\ y e. On /\ ( y e. G -> ( R1 ` y ) e. G ) ) /\ suc y e. G ) -> suc y e. G )
30 sssucid 
 |-  y C_ suc y
31 30 a1i 
 |-  ( ( ( ( ph /\ A e. On ) /\ y e. On /\ ( y e. G -> ( R1 ` y ) e. G ) ) /\ suc y e. G ) -> y C_ suc y )
32 gruss 
 |-  ( ( G e. Univ /\ suc y e. G /\ y C_ suc y ) -> y e. G )
33 28 29 31 32 syl3anc 
 |-  ( ( ( ( ph /\ A e. On ) /\ y e. On /\ ( y e. G -> ( R1 ` y ) e. G ) ) /\ suc y e. G ) -> y e. G )
34 simpl3 
 |-  ( ( ( ( ph /\ A e. On ) /\ y e. On /\ ( y e. G -> ( R1 ` y ) e. G ) ) /\ suc y e. G ) -> ( y e. G -> ( R1 ` y ) e. G ) )
35 33 34 mpd 
 |-  ( ( ( ( ph /\ A e. On ) /\ y e. On /\ ( y e. G -> ( R1 ` y ) e. G ) ) /\ suc y e. G ) -> ( R1 ` y ) e. G )
36 r1suc 
 |-  ( y e. On -> ( R1 ` suc y ) = ~P ( R1 ` y ) )
37 36 3ad2ant2 
 |-  ( ( ( ph /\ A e. On ) /\ y e. On /\ ( R1 ` y ) e. G ) -> ( R1 ` suc y ) = ~P ( R1 ` y ) )
38 27 3ad2ant1 
 |-  ( ( ( ph /\ A e. On ) /\ y e. On /\ ( R1 ` y ) e. G ) -> G e. Univ )
39 simp3 
 |-  ( ( ( ph /\ A e. On ) /\ y e. On /\ ( R1 ` y ) e. G ) -> ( R1 ` y ) e. G )
40 grupw 
 |-  ( ( G e. Univ /\ ( R1 ` y ) e. G ) -> ~P ( R1 ` y ) e. G )
41 38 39 40 syl2anc 
 |-  ( ( ( ph /\ A e. On ) /\ y e. On /\ ( R1 ` y ) e. G ) -> ~P ( R1 ` y ) e. G )
42 37 41 eqeltrd 
 |-  ( ( ( ph /\ A e. On ) /\ y e. On /\ ( R1 ` y ) e. G ) -> ( R1 ` suc y ) e. G )
43 25 26 35 42 syl3anc 
 |-  ( ( ( ( ph /\ A e. On ) /\ y e. On /\ ( y e. G -> ( R1 ` y ) e. G ) ) /\ suc y e. G ) -> ( R1 ` suc y ) e. G )
44 43 ex 
 |-  ( ( ( ph /\ A e. On ) /\ y e. On /\ ( y e. G -> ( R1 ` y ) e. G ) ) -> ( suc y e. G -> ( R1 ` suc y ) e. G ) )
45 simpr 
 |-  ( ( ( ( ph /\ A e. On ) /\ Lim x /\ A. y e. x ( y e. G -> ( R1 ` y ) e. G ) ) /\ x e. G ) -> x e. G )
46 simpl2 
 |-  ( ( ( ( ph /\ A e. On ) /\ Lim x /\ A. y e. x ( y e. G -> ( R1 ` y ) e. G ) ) /\ x e. G ) -> Lim x )
47 r1lim 
 |-  ( ( x e. G /\ Lim x ) -> ( R1 ` x ) = U_ y e. x ( R1 ` y ) )
48 45 46 47 syl2anc 
 |-  ( ( ( ( ph /\ A e. On ) /\ Lim x /\ A. y e. x ( y e. G -> ( R1 ` y ) e. G ) ) /\ x e. G ) -> ( R1 ` x ) = U_ y e. x ( R1 ` y ) )
49 simpl1 
 |-  ( ( ( ( ph /\ A e. On ) /\ Lim x /\ A. y e. x ( y e. G -> ( R1 ` y ) e. G ) ) /\ x e. G ) -> ( ph /\ A e. On ) )
50 49 27 syl 
 |-  ( ( ( ( ph /\ A e. On ) /\ Lim x /\ A. y e. x ( y e. G -> ( R1 ` y ) e. G ) ) /\ x e. G ) -> G e. Univ )
51 simpl3 
 |-  ( ( ( ( ph /\ A e. On ) /\ Lim x /\ A. y e. x ( y e. G -> ( R1 ` y ) e. G ) ) /\ x e. G ) -> A. y e. x ( y e. G -> ( R1 ` y ) e. G ) )
52 simpl1l 
 |-  ( ( ( ( ph /\ A e. On ) /\ Lim x /\ A. y e. x ( y e. G -> ( R1 ` y ) e. G ) ) /\ x e. G ) -> ph )
53 simpl1 
 |-  ( ( ( ph /\ Lim x /\ x e. G ) /\ y e. x ) -> ph )
54 53 1 syl 
 |-  ( ( ( ph /\ Lim x /\ x e. G ) /\ y e. x ) -> G e. Univ )
55 simpl3 
 |-  ( ( ( ph /\ Lim x /\ x e. G ) /\ y e. x ) -> x e. G )
56 simpl2 
 |-  ( ( ( ph /\ Lim x /\ x e. G ) /\ y e. x ) -> Lim x )
57 limord 
 |-  ( Lim x -> Ord x )
58 56 57 syl 
 |-  ( ( ( ph /\ Lim x /\ x e. G ) /\ y e. x ) -> Ord x )
59 simpr 
 |-  ( ( ( ph /\ Lim x /\ x e. G ) /\ y e. x ) -> y e. x )
60 ordelss 
 |-  ( ( Ord x /\ y e. x ) -> y C_ x )
61 58 59 60 syl2anc 
 |-  ( ( ( ph /\ Lim x /\ x e. G ) /\ y e. x ) -> y C_ x )
62 gruss 
 |-  ( ( G e. Univ /\ x e. G /\ y C_ x ) -> y e. G )
63 54 55 61 62 syl3anc 
 |-  ( ( ( ph /\ Lim x /\ x e. G ) /\ y e. x ) -> y e. G )
64 63 ralrimiva 
 |-  ( ( ph /\ Lim x /\ x e. G ) -> A. y e. x y e. G )
65 52 46 45 64 syl3anc 
 |-  ( ( ( ( ph /\ A e. On ) /\ Lim x /\ A. y e. x ( y e. G -> ( R1 ` y ) e. G ) ) /\ x e. G ) -> A. y e. x y e. G )
66 ralim 
 |-  ( A. y e. x ( y e. G -> ( R1 ` y ) e. G ) -> ( A. y e. x y e. G -> A. y e. x ( R1 ` y ) e. G ) )
67 51 65 66 sylc 
 |-  ( ( ( ( ph /\ A e. On ) /\ Lim x /\ A. y e. x ( y e. G -> ( R1 ` y ) e. G ) ) /\ x e. G ) -> A. y e. x ( R1 ` y ) e. G )
68 gruiun 
 |-  ( ( G e. Univ /\ x e. G /\ A. y e. x ( R1 ` y ) e. G ) -> U_ y e. x ( R1 ` y ) e. G )
69 50 45 67 68 syl3anc 
 |-  ( ( ( ( ph /\ A e. On ) /\ Lim x /\ A. y e. x ( y e. G -> ( R1 ` y ) e. G ) ) /\ x e. G ) -> U_ y e. x ( R1 ` y ) e. G )
70 48 69 eqeltrd 
 |-  ( ( ( ( ph /\ A e. On ) /\ Lim x /\ A. y e. x ( y e. G -> ( R1 ` y ) e. G ) ) /\ x e. G ) -> ( R1 ` x ) e. G )
71 70 ex 
 |-  ( ( ( ph /\ A e. On ) /\ Lim x /\ A. y e. x ( y e. G -> ( R1 ` y ) e. G ) ) -> ( x e. G -> ( R1 ` x ) e. G ) )
72 simpr 
 |-  ( ( ph /\ A e. On ) -> A e. On )
73 7 11 15 19 24 44 71 72 tfindsd 
 |-  ( ( ph /\ A e. On ) -> ( A e. G -> ( R1 ` A ) e. G ) )
74 3 73 mpd 
 |-  ( ( ph /\ A e. On ) -> ( R1 ` A ) e. G )
75 r1fnon 
 |-  R1 Fn On
76 75 fndmi 
 |-  dom R1 = On
77 76 eleq2i 
 |-  ( A e. dom R1 <-> A e. On )
78 ndmfv 
 |-  ( -. A e. dom R1 -> ( R1 ` A ) = (/) )
79 77 78 sylnbir 
 |-  ( -. A e. On -> ( R1 ` A ) = (/) )
80 79 adantl 
 |-  ( ( ph /\ -. A e. On ) -> ( R1 ` A ) = (/) )
81 21 adantr 
 |-  ( ( ph /\ -. A e. On ) -> (/) e. G )
82 80 81 eqeltrd 
 |-  ( ( ph /\ -. A e. On ) -> ( R1 ` A ) e. G )
83 74 82 pm2.61dan 
 |-  ( ph -> ( R1 ` A ) e. G )