Metamath Proof Explorer


Theorem gruscottcld

Description: If a Grothendieck universe contains an element of a Scott's trick set, it contains the Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023)

Ref Expression
Hypotheses gruscottcld.1 φ G Univ
gruscottcld.2 φ B G
gruscottcld.3 φ B Scott A
Assertion gruscottcld φ Scott A G

Proof

Step Hyp Ref Expression
1 gruscottcld.1 φ G Univ
2 gruscottcld.2 φ B G
3 gruscottcld.3 φ B Scott A
4 3 scottrankd φ rank Scott A = suc rank B
5 1 2 grurankcld φ rank B G
6 1 5 grusucd φ suc rank B G
7 4 6 eqeltrd φ rank Scott A G
8 scottex2 Scott A V
9 8 a1i φ Scott A V
10 1 7 9 grurankrcld φ Scott A G