mnugrud

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

	Ref	Expression
Hypotheses	mnugrud.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))))\}$
	mnugrud.2	$⊢ φ \to U \in M$
Assertion	mnugrud	$⊢ φ \to U \in Univ$

Proof

Step	Hyp	Ref	Expression
1		mnugrud.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		mnugrud.2	$⊢ φ \to U \in M$
3	1 2	mnutrd	$⊢ φ \to Tr U$
4	2	adantr	$⊢ (φ \land x \in U) \to U \in M$
5		simpr	$⊢ (φ \land x \in U) \to x \in U$
6	1 4 5	mnupwd	$⊢ (φ \land x \in U) \to 𝒫 x \in U$
7	2	ad2antrr	$⊢ ((φ \land x \in U) \land y \in U) \to U \in M$
8	5	adantr	$⊢ ((φ \land x \in U) \land y \in U) \to x \in U$
9		simpr	$⊢ ((φ \land x \in U) \land y \in U) \to y \in U$
10	1 7 8 9	mnuprd	$⊢ ((φ \land x \in U) \land y \in U) \to \{x, y\} \in U$
11	10	ralrimiva	$⊢ (φ \land x \in U) \to \forall y \in U \{x, y\} \in U$
12	2	ad2antrr	$⊢ ((φ \land x \in U) \land y \in (U^{x})) \to U \in M$
13	5	adantr	$⊢ ((φ \land x \in U) \land y \in (U^{x})) \to x \in U$
14		elmapi	$⊢ y \in (U^{x}) \to y : x ⟶ U$
15	14	adantl	$⊢ ((φ \land x \in U) \land y \in (U^{x})) \to y : x ⟶ U$
16	1 12 13 15	mnurnd	$⊢ ((φ \land x \in U) \land y \in (U^{x})) \to ran y \in U$
17	1 12 16	mnuunid	$⊢ ((φ \land x \in U) \land y \in (U^{x})) \to ⋃ ran y \in U$
18	17	ralrimiva	$⊢ (φ \land x \in U) \to \forall y \in (U^{x}) ⋃ ran y \in U$
19	6 11 18	3jca	$⊢ (φ \land x \in U) \to (𝒫 x \in U \land \forall y \in U \{x, y\} \in U \land \forall y \in (U^{x}) ⋃ ran y \in U)$
20	19	ralrimiva	$⊢ φ \to \forall x \in U (𝒫 x \in U \land \forall y \in U \{x, y\} \in U \land \forall y \in (U^{x}) ⋃ ran y \in U)$
21		elgrug	$⊢ U \in M \to (U \in Univ \leftrightarrow (Tr U \land \forall x \in U (𝒫 x \in U \land \forall y \in U \{x, y\} \in U \land \forall y \in (U^{x}) ⋃ ran y \in U)))$
22	2 21	syl	$⊢ φ \to (U \in Univ \leftrightarrow (Tr U \land \forall x \in U (𝒫 x \in U \land \forall y \in U \{x, y\} \in U \land \forall y \in (U^{x}) ⋃ ran y \in U)))$
23	3 20 22	mpbir2and	$⊢ φ \to U \in Univ$

Metamath Proof Explorer

Theorem mnugrud

Proof