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	$⊢ φ \to I \in Inacc$
	Assertion	inagrud	$⊢ φ \to R_{1} (I) \in Univ$

Step	Hyp	Ref	Expression
1		inagrud.1	$⊢ φ \to I \in Inacc$
2		inatsk	$⊢ I \in Inacc \to R_{1} (I) \in Tarski$
3	1 2	syl	$⊢ φ \to R_{1} (I) \in Tarski$
4		r1tr	$⊢ Tr R_{1} (I)$
5		grutsk1	$⊢ (R_{1} (I) \in Tarski \land Tr R_{1} (I)) \to R_{1} (I) \in Univ$
6	3 4 5	sylancl	$⊢ φ \to R_{1} (I) \in Univ$