Description: Inaccessible levels of the cumulative hierarchy are Grothendieck universes. (Contributed by Rohan Ridenour, 13-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Hypothesis | inagrud.1 | ||
Assertion | inagrud |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inagrud.1 | ||
2 | inatsk | ||
3 | 1 2 | syl | |
4 | r1tr | ||
5 | grutsk1 | ||
6 | 3 4 5 | sylancl |