Metamath Proof Explorer

Theorem mnurnd

Description: Minimal universes contain ranges of functions from an element of the universe to the universe. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses mnurnd.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
mnurnd.2 ⊢ φ → U ∈ M
mnurnd.3 ⊢ φ → A ∈ U
mnurnd.4 ⊢ φ → F : A ⟶ U
Assertion mnurnd ⊢ φ → ran ⁡ F ∈ U

Proof

Step Hyp Ref Expression
1 mnurnd.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 mnurnd.2 ⊢ φ → U ∈ M
3 mnurnd.3 ⊢ φ → A ∈ U
4 mnurnd.4 ⊢ φ → F : A ⟶ U
5 3 elexd ⊢ φ → A ∈ V
6 5 iftrued ⊢ φ → if A ∈ V A ∅ = A
7 6 3 eqeltrd ⊢ φ → if A ∈ V A ∅ ∈ U
8 6 feq2d ⊢ φ → F : if A ∈ V A ∅ ⟶ U ↔ F : A ⟶ U
9 4 8 mpbird ⊢ φ → F : if A ∈ V A ∅ ⟶ U
10 0ex ⊢ ∅ ∈ V
11 10 elimel ⊢ if A ∈ V A ∅ ∈ V
12 1 2 7 9 11 mnurndlem2 ⊢ φ → ran ⁡ F ∈ U