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 \| \forall l \in k (𝒫 l \subseteq k \land \forall m \exists n \in k (𝒫 l \subseteq n \land \forall p \in l (\exists q \in k (p \in q \land q \in m) \to \exists r \in m (p \in r \land ⋃ r \subseteq n))))\}$
		mnurnd.2	$⊢ φ \to U \in M$
		mnurnd.3	$⊢ φ \to A \in U$
		mnurnd.4	$⊢ φ \to F : A ⟶ U$
	Assertion	mnurnd	$⊢ φ \to ran F \in U$

Proof

Step	Hyp	Ref	Expression
1		mnurnd.1	$⊢ M = \{k \| \forall l \in k (𝒫 l \subseteq k \land \forall m \exists n \in k (𝒫 l \subseteq n \land \forall p \in l (\exists q \in k (p \in q \land q \in m) \to \exists r \in m (p \in r \land ⋃ r \subseteq n))))\}$
2		mnurnd.2	$⊢ φ \to U \in M$
3		mnurnd.3	$⊢ φ \to A \in U$
4		mnurnd.4	$⊢ φ \to F : A ⟶ U$
5	3	elexd	$⊢ φ \to A \in V$
6	5	iftrued	$⊢ φ \to if (A \in V, A, \emptyset) = A$
7	6 3	eqeltrd	$⊢ φ \to if (A \in V, A, \emptyset) \in U$
8	6	feq2d	$⊢ φ \to (F : if (A \in V, A, \emptyset) ⟶ U \leftrightarrow F : A ⟶ U)$
9	4 8	mpbird	$⊢ φ \to F : if (A \in V, A, \emptyset) ⟶ U$
10		0ex	$⊢ \emptyset \in V$
11	10	elimel	$⊢ if (A \in V, A, \emptyset) \in V$
12	1 2 7 9 11	mnurndlem2	$⊢ φ \to ran F \in U$