Theorem grusucd

Description: Grothendieck universes are closed under ordinal successor. (Contributed by Rohan Ridenour, 9-Aug-2023)

	Ref	Expression
Hypotheses	grusucd.1	|- ( ph -> G e. Univ )
	grusucd.2	|- ( ph -> A e. G )
Assertion	grusucd	|- ( ph -> suc A e. G )

Proof

Step	Hyp	Ref	Expression
1		grusucd.1	|- ( ph -> G e. Univ )
2		grusucd.2	|- ( ph -> A e. G )
3		df-suc	|- suc A = ( A u. { A } )
4		grusn	|- ( ( G e. Univ /\ A e. G ) -> { A } e. G )
5	1 2 4	syl2anc	|- ( ph -> { A } e. G )
6		gruun	|- ( ( G e. Univ /\ A e. G /\ { A } e. G ) -> ( A u. { A } ) e. G )
7	1 2 5 6	syl3anc	|- ( ph -> ( A u. { A } ) e. G )
8	3 7	eqeltrid	|- ( ph -> suc A e. G )