Theorem inagrud

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

	Ref	Expression
Hypothesis	inagrud.1	⊢ ( 𝜑 → 𝐼 ∈ Inacc )
Assertion	inagrud	⊢ ( 𝜑 → ( 𝑅1 ‘ 𝐼 ) ∈ Univ )

Proof

Step	Hyp	Ref	Expression
1		inagrud.1	⊢ ( 𝜑 → 𝐼 ∈ Inacc )
2		inatsk	⊢ ( 𝐼 ∈ Inacc → ( 𝑅1 ‘ 𝐼 ) ∈ Tarski )
3	1 2	syl	⊢ ( 𝜑 → ( 𝑅1 ‘ 𝐼 ) ∈ Tarski )
4		r1tr	⊢ Tr ( 𝑅1 ‘ 𝐼 )
5		grutsk1	⊢ ( ( ( 𝑅1 ‘ 𝐼 ) ∈ Tarski ∧ Tr ( 𝑅1 ‘ 𝐼 ) ) → ( 𝑅1 ‘ 𝐼 ) ∈ Univ )
6	3 4 5	sylancl	⊢ ( 𝜑 → ( 𝑅1 ‘ 𝐼 ) ∈ Univ )