Metamath Proof Explorer

Theorem grutr

Description: A Grothendieck universe is transitive. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion grutr ⊢ U ∈ Univ → Tr ⁡ U

Proof

Step Hyp Ref Expression
1 elgrug ⊢ U ∈ Univ → U ∈ Univ ↔ Tr ⁡ U ∧ ∀ x ∈ U 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U
2 1 ibi ⊢ U ∈ Univ → Tr ⁡ U ∧ ∀ x ∈ U 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U
3 2 simpld ⊢ U ∈ Univ → Tr ⁡ U