Metamath Proof Explorer

Theorem wuntr

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

Ref Expression
Assertion wuntr ⊢ U ∈ WUni → Tr ⁡ U

Proof

Step Hyp Ref Expression
1 iswun ⊢ U ∈ WUni → U ∈ WUni ↔ Tr ⁡ U ∧ U ≠ ∅ ∧ ∀ x ∈ U ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U
2 1 ibi ⊢ U ∈ WUni → Tr ⁡ U ∧ U ≠ ∅ ∧ ∀ x ∈ U ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U
3 2 simp1d ⊢ U ∈ WUni → Tr ⁡ U