Metamath Proof Explorer


Theorem inagrud

Description: Inaccessible levels of the cumulative hierarchy are Grothendieck universes. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypothesis inagrud.1 φ I Inacc
Assertion inagrud φ R1 I Univ

Proof

Step Hyp Ref Expression
1 inagrud.1 φ I Inacc
2 inatsk I Inacc R1 I Tarski
3 1 2 syl φ R1 I Tarski
4 r1tr Tr R1 I
5 grutsk1 R1 I Tarski Tr R1 I R1 I Univ
6 3 4 5 sylancl φ R1 I Univ