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 ( 𝜑𝐺 ∈ Univ )
gruscottcld.2 ( 𝜑𝐵𝐺 )
gruscottcld.3 ( 𝜑𝐵 ∈ Scott 𝐴 )
Assertion gruscottcld ( 𝜑 → Scott 𝐴𝐺 )

Proof

Step Hyp Ref Expression
1 gruscottcld.1 ( 𝜑𝐺 ∈ Univ )
2 gruscottcld.2 ( 𝜑𝐵𝐺 )
3 gruscottcld.3 ( 𝜑𝐵 ∈ Scott 𝐴 )
4 3 scottrankd ( 𝜑 → ( rank ‘ Scott 𝐴 ) = suc ( rank ‘ 𝐵 ) )
5 1 2 grurankcld ( 𝜑 → ( rank ‘ 𝐵 ) ∈ 𝐺 )
6 1 5 grusucd ( 𝜑 → suc ( rank ‘ 𝐵 ) ∈ 𝐺 )
7 4 6 eqeltrd ( 𝜑 → ( rank ‘ Scott 𝐴 ) ∈ 𝐺 )
8 scottex2 Scott 𝐴 ∈ V
9 8 a1i ( 𝜑 → Scott 𝐴 ∈ V )
10 1 7 9 grurankrcld ( 𝜑 → Scott 𝐴𝐺 )