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 φ G Univ
grur1cld.2 φ A G
Assertion grur1cld φ R1 A G

Proof

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