grumnud

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

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

Proof

Step	Hyp	Ref	Expression
1		grumnud.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		grumnud.2	$⊢ φ \to G \in Univ$
3		eqid	$⊢ \{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G) = \{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)$
4		brxp	$⊢ i (G \times G) h \leftrightarrow (i \in G \land h \in G)$
5		brin	$⊢ i (\{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)) h \leftrightarrow (i \{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} h \land i (G \times G) h)$
6	5	rbaib	$⊢ i (G \times G) h \to (i (\{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)) h \leftrightarrow i \{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} h)$
7	4 6	sylbir	$⊢ (i \in G \land h \in G) \to (i (\{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)) h \leftrightarrow i \{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} h)$
8		vex	$⊢ i \in V$
9		vex	$⊢ h \in V$
10		simpr	$⊢ ((b = i \land c = h) \land d = j) \to d = j$
11	10	unieqd	$⊢ ((b = i \land c = h) \land d = j) \to ⋃ d = ⋃ j$
12		simplr	$⊢ ((b = i \land c = h) \land d = j) \to c = h$
13	11 12	eqeq12d	$⊢ ((b = i \land c = h) \land d = j) \to (⋃ d = c \leftrightarrow ⋃ j = h)$
14		elequ1	$⊢ d = j \to (d \in f \leftrightarrow j \in f)$
15	14	adantl	$⊢ ((b = i \land c = h) \land d = j) \to (d \in f \leftrightarrow j \in f)$
16		eleq12	$⊢ (b = i \land d = j) \to (b \in d \leftrightarrow i \in j)$
17	16	adantlr	$⊢ ((b = i \land c = h) \land d = j) \to (b \in d \leftrightarrow i \in j)$
18	13 15 17	3anbi123d	$⊢ ((b = i \land c = h) \land d = j) \to ((⋃ d = c \land d \in f \land b \in d) \leftrightarrow (⋃ j = h \land j \in f \land i \in j))$
19	18	cbvexdvaw	$⊢ (b = i \land c = h) \to (\exists d (⋃ d = c \land d \in f \land b \in d) \leftrightarrow \exists j (⋃ j = h \land j \in f \land i \in j))$
20		eqid	$⊢ \{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} = \{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\}$
21	8 9 19 20	braba	$⊢ i \{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} h \leftrightarrow \exists j (⋃ j = h \land j \in f \land i \in j)$
22	7 21	bitrdi	$⊢ (i \in G \land h \in G) \to (i (\{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)) h \leftrightarrow \exists j (⋃ j = h \land j \in f \land i \in j))$
23		simplr3	$⊢ ((h \in ((\{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)) Coll z) \land (⋃ j = h \land j \in f \land i \in j)) \land u = j) \to i \in j$
24		simpr	$⊢ ((h \in ((\{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)) Coll z) \land (⋃ j = h \land j \in f \land i \in j)) \land u = j) \to u = j$
25	23 24	eleqtrrd	$⊢ ((h \in ((\{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)) Coll z) \land (⋃ j = h \land j \in f \land i \in j)) \land u = j) \to i \in u$
26	24	unieqd	$⊢ ((h \in ((\{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)) Coll z) \land (⋃ j = h \land j \in f \land i \in j)) \land u = j) \to ⋃ u = ⋃ j$
27		simplr1	$⊢ ((h \in ((\{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)) Coll z) \land (⋃ j = h \land j \in f \land i \in j)) \land u = j) \to ⋃ j = h$
28	26 27	eqtrd	$⊢ ((h \in ((\{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)) Coll z) \land (⋃ j = h \land j \in f \land i \in j)) \land u = j) \to ⋃ u = h$
29		simpll	$⊢ ((h \in ((\{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)) Coll z) \land (⋃ j = h \land j \in f \land i \in j)) \land u = j) \to h \in ((\{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)) Coll z)$
30	28 29	eqeltrd	$⊢ ((h \in ((\{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)) Coll z) \land (⋃ j = h \land j \in f \land i \in j)) \land u = j) \to ⋃ u \in ((\{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)) Coll z)$
31	25 30	jca	$⊢ ((h \in ((\{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)) Coll z) \land (⋃ j = h \land j \in f \land i \in j)) \land u = j) \to (i \in u \land ⋃ u \in ((\{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)) Coll z))$
32		simpr2	$⊢ (h \in ((\{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)) Coll z) \land (⋃ j = h \land j \in f \land i \in j)) \to j \in f$
33	31 32	rspcime	$⊢ (h \in ((\{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)) Coll z) \land (⋃ j = h \land j \in f \land i \in j)) \to \exists u \in f (i \in u \land ⋃ u \in ((\{⟨b, c⟩ \| \exists d (⋃ d = c \land d \in f \land b \in d)\} \cap (G \times G)) Coll z))$
34	1 2 3 22 33	grumnudlem	$⊢ φ \to G \in M$

Metamath Proof Explorer

Theorem grumnud

Proof