Metamath Proof Explorer

Theorem gruwun

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

Ref Expression
Assertion gruwun ⊢ U ∈ Univ ∧ U ≠ ∅ → U ∈ WUni

Proof

Step Hyp Ref Expression
1 grutr ⊢ U ∈ Univ → Tr ⁡ U
2 1 adantr ⊢ U ∈ Univ ∧ U ≠ ∅ → Tr ⁡ U
3 simpr ⊢ U ∈ Univ ∧ U ≠ ∅ → U ≠ ∅
4 gruuni ⊢ U ∈ Univ ∧ x ∈ U → ⋃ x ∈ U
5 4 adantlr ⊢ U ∈ Univ ∧ U ≠ ∅ ∧ x ∈ U → ⋃ x ∈ U
6 grupw ⊢ U ∈ Univ ∧ x ∈ U → 𝒫 x ∈ U
7 6 adantlr ⊢ U ∈ Univ ∧ U ≠ ∅ ∧ x ∈ U → 𝒫 x ∈ U
8 grupr ⊢ U ∈ Univ ∧ x ∈ U ∧ y ∈ U → x y ∈ U
9 8 ad4ant134 ⊢ U ∈ Univ ∧ U ≠ ∅ ∧ x ∈ U ∧ y ∈ U → x y ∈ U
10 9 ralrimiva ⊢ U ∈ Univ ∧ U ≠ ∅ ∧ x ∈ U → ∀ y ∈ U x y ∈ U
11 5 7 10 3jca ⊢ U ∈ Univ ∧ U ≠ ∅ ∧ x ∈ U → ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U
12 11 ralrimiva ⊢ U ∈ Univ ∧ U ≠ ∅ → ∀ x ∈ U ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U
13 iswun ⊢ U ∈ Univ → U ∈ WUni ↔ Tr ⁡ U ∧ U ≠ ∅ ∧ ∀ x ∈ U ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U
14 13 adantr ⊢ U ∈ Univ ∧ U ≠ ∅ → U ∈ WUni ↔ Tr ⁡ U ∧ U ≠ ∅ ∧ ∀ x ∈ U ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U
15 2 3 12 14 mpbir3and ⊢ U ∈ Univ ∧ U ≠ ∅ → U ∈ WUni