Theorem grusucd

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

	Ref	Expression
Hypotheses	grusucd.1	⊢ ( 𝜑 → 𝐺 ∈ Univ )
	grusucd.2	⊢ ( 𝜑 → 𝐴 ∈ 𝐺 )
Assertion	grusucd	⊢ ( 𝜑 → suc 𝐴 ∈ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		grusucd.1	⊢ ( 𝜑 → 𝐺 ∈ Univ )
2		grusucd.2	⊢ ( 𝜑 → 𝐴 ∈ 𝐺 )
3		df-suc	⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
4		grusn	⊢ ( ( 𝐺 ∈ Univ ∧ 𝐴 ∈ 𝐺 ) → { 𝐴 } ∈ 𝐺 )
5	1 2 4	syl2anc	⊢ ( 𝜑 → { 𝐴 } ∈ 𝐺 )
6		gruun	⊢ ( ( 𝐺 ∈ Univ ∧ 𝐴 ∈ 𝐺 ∧ { 𝐴 } ∈ 𝐺 ) → ( 𝐴 ∪ { 𝐴 } ) ∈ 𝐺 )
7	1 2 5 6	syl3anc	⊢ ( 𝜑 → ( 𝐴 ∪ { 𝐴 } ) ∈ 𝐺 )
8	3 7	eqeltrid	⊢ ( 𝜑 → suc 𝐴 ∈ 𝐺 )