Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Rohan Ridenour
Shorter primitive equivalent of ax-groth
Grothendieck universes are closed under collection
gruscottcld
Metamath Proof Explorer
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 𝐴 ∈ 𝐺 )