Metamath Proof Explorer

Theorem mnugrud

Description: Minimal universes are Grothendieck universes. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses mnugrud.1 ⊢ M = k | ∀ l ∈ k 𝒫 l ⊆ k ∧ ∀ m ∃ n ∈ k 𝒫 l ⊆ n ∧ ∀ p ∈ l ∃ q ∈ k p ∈ q ∧ q ∈ m → ∃ r ∈ m p ∈ r ∧ ⋃ r ⊆ n
mnugrud.2 ⊢ φ → U ∈ M
Assertion mnugrud ⊢ φ → U ∈ Univ

Proof

Step Hyp Ref Expression
1 mnugrud.1 ⊢ M = k | ∀ l ∈ k 𝒫 l ⊆ k ∧ ∀ m ∃ n ∈ k 𝒫 l ⊆ n ∧ ∀ p ∈ l ∃ q ∈ k p ∈ q ∧ q ∈ m → ∃ r ∈ m p ∈ r ∧ ⋃ r ⊆ n
2 mnugrud.2 ⊢ φ → U ∈ M
3 1 2 mnutrd ⊢ φ → Tr ⁡ U
4 2 adantr ⊢ φ ∧ x ∈ U → U ∈ M
5 simpr ⊢ φ ∧ x ∈ U → x ∈ U
6 1 4 5 mnupwd ⊢ φ ∧ x ∈ U → 𝒫 x ∈ U
7 2 ad2antrr ⊢ φ ∧ x ∈ U ∧ y ∈ U → U ∈ M
8 5 adantr ⊢ φ ∧ x ∈ U ∧ y ∈ U → x ∈ U
9 simpr ⊢ φ ∧ x ∈ U ∧ y ∈ U → y ∈ U
10 1 7 8 9 mnuprd ⊢ φ ∧ x ∈ U ∧ y ∈ U → x y ∈ U
11 10 ralrimiva ⊢ φ ∧ x ∈ U → ∀ y ∈ U x y ∈ U
12 2 ad2antrr ⊢ φ ∧ x ∈ U ∧ y ∈ U x → U ∈ M
13 5 adantr ⊢ φ ∧ x ∈ U ∧ y ∈ U x → x ∈ U
14 elmapi ⊢ y ∈ U x → y : x ⟶ U
15 14 adantl ⊢ φ ∧ x ∈ U ∧ y ∈ U x → y : x ⟶ U
16 1 12 13 15 mnurnd ⊢ φ ∧ x ∈ U ∧ y ∈ U x → ran ⁡ y ∈ U
17 1 12 16 mnuunid ⊢ φ ∧ x ∈ U ∧ y ∈ U x → ⋃ ran ⁡ y ∈ U
18 17 ralrimiva ⊢ φ ∧ x ∈ U → ∀ y ∈ U x ⋃ ran ⁡ y ∈ U
19 6 11 18 3jca ⊢ φ ∧ x ∈ U → 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U
20 19 ralrimiva ⊢ φ → ∀ x ∈ U 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U
21 elgrug ⊢ U ∈ M → U ∈ Univ ↔ Tr ⁡ U ∧ ∀ x ∈ U 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U
22 2 21 syl ⊢ φ → U ∈ Univ ↔ Tr ⁡ U ∧ ∀ x ∈ U 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U
23 3 20 22 mpbir2and ⊢ φ → U ∈ Univ