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 ⊢ ( 𝜑 → 𝐺 ∈ Univ )
grur1cld.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝐺 )
Assertion grur1cld ( 𝜑 → ( 𝑅1 ‘ 𝐴 ) ∈ 𝐺 )

Proof

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