Metamath Proof Explorer


Theorem grusucd

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

Ref Expression
Hypotheses grusucd.1 φ G Univ
grusucd.2 φ A G
Assertion grusucd φ suc A G

Proof

Step Hyp Ref Expression
1 grusucd.1 φ G Univ
2 grusucd.2 φ A G
3 df-suc suc A = A A
4 grusn G Univ A G A G
5 1 2 4 syl2anc φ A G
6 gruun G Univ A G A G A A G
7 1 2 5 6 syl3anc φ A A G
8 3 7 eqeltrid φ suc A G