Theorem grusucd

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

	Ref	Expression
Hypotheses	grusucd.1	$$⊢\phi \to G\in \mathrm{Univ}$$
	grusucd.2	$$⊢\phi \to A\in G$$
Assertion	grusucd	$$⊢\phi \to \mathrm{suc}A\in G$$

Proof

Step	Hyp	Ref	Expression
1		grusucd.1	$$⊢\phi \to G\in \mathrm{Univ}$$
2		grusucd.2	$$⊢\phi \to A\in G$$
3		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
4		grusn	$$⊢\left(G\in \mathrm{Univ}\wedge A\in G\right)\to \left\{A\right\}\in G$$
5	1 2 4	syl2anc	$$⊢\phi \to \left\{A\right\}\in G$$
6		gruun	$$⊢\left(G\in \mathrm{Univ}\wedge A\in G\wedge \left\{A\right\}\in G\right)\to A\cup \left\{A\right\}\in G$$
7	1 2 5 6	syl3anc	$$⊢\phi \to A\cup \left\{A\right\}\in G$$
8	3 7	eqeltrid	$$⊢\phi \to \mathrm{suc}A\in G$$