Theorem inagrud

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

	Ref	Expression
Hypothesis	inagrud.1	|- ( ph -> I e. Inacc )
Assertion	inagrud	|- ( ph -> ( R1 ` I ) e. Univ )

Proof

Step	Hyp	Ref	Expression
1		inagrud.1	|- ( ph -> I e. Inacc )
2		inatsk	|- ( I e. Inacc -> ( R1 ` I ) e. Tarski )
3	1 2	syl	|- ( ph -> ( R1 ` I ) e. Tarski )
4		r1tr	|- Tr ( R1 ` I )
5		grutsk1	|- ( ( ( R1 ` I ) e. Tarski /\ Tr ( R1 ` I ) ) -> ( R1 ` I ) e. Univ )
6	3 4 5	sylancl	|- ( ph -> ( R1 ` I ) e. Univ )