ismnu

Description: The hypothesis of this theorem defines a class M of sets that we temporarily call "minimal universes", and which will turn out in grumnueq to be exactly Grothendicek universes. Minimal universes are sets which satisfy the predicate on y in rr-groth , except for the x e. y clause.

A minimal universe is closed under subsets ( mnussd ), powersets ( mnupwd ), and an operation which is similar to a combination of collection and union ( mnuop3d ), from which closure under pairing ( mnuprd ), unions ( mnuunid ), and function ranges ( mnurnd ) can be deduced, from which equivalence with Grothendieck universes ( grumnueq ) can be deduced. (Contributed by Rohan Ridenour, 13-Aug-2023)

		Ref	Expression
	Hypothesis	ismnu.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))))\}$
	Assertion	ismnu	$⊢ U \in V \to (U \in M \leftrightarrow \forall z \in U (𝒫 z \subseteq U \land \forall f \exists w \in U (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))))$

Proof

Step	Hyp	Ref	Expression
1		ismnu.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		simpr	$⊢ (k = U \land l = z) \to l = z$
3	2	pweqd	$⊢ (k = U \land l = z) \to 𝒫 l = 𝒫 z$
4		simpl	$⊢ (k = U \land l = z) \to k = U$
5	3 4	sseq12d	$⊢ (k = U \land l = z) \to (𝒫 l \subseteq k \leftrightarrow 𝒫 z \subseteq U)$
6	3	3adant3	$⊢ (k = U \land l = z \land m = f) \to 𝒫 l = 𝒫 z$
7	6	adantr	$⊢ ((k = U \land l = z \land m = f) \land n = w) \to 𝒫 l = 𝒫 z$
8		simpr	$⊢ ((k = U \land l = z \land m = f) \land n = w) \to n = w$
9	7 8	sseq12d	$⊢ ((k = U \land l = z \land m = f) \land n = w) \to (𝒫 l \subseteq n \leftrightarrow 𝒫 z \subseteq w)$
10		simpl3	$⊢ (((k = U \land l = z \land m = f) \land n = w \land p = i) \land q = v) \to p = i$
11		simpr	$⊢ (((k = U \land l = z \land m = f) \land n = w \land p = i) \land q = v) \to q = v$
12	10 11	eleq12d	$⊢ (((k = U \land l = z \land m = f) \land n = w \land p = i) \land q = v) \to (p \in q \leftrightarrow i \in v)$
13		simpl13	$⊢ (((k = U \land l = z \land m = f) \land n = w \land p = i) \land q = v) \to m = f$
14	11 13	eleq12d	$⊢ (((k = U \land l = z \land m = f) \land n = w \land p = i) \land q = v) \to (q \in m \leftrightarrow v \in f)$
15	12 14	anbi12d	$⊢ (((k = U \land l = z \land m = f) \land n = w \land p = i) \land q = v) \to ((p \in q \land q \in m) \leftrightarrow (i \in v \land v \in f))$
16		simpl11	$⊢ (((k = U \land l = z \land m = f) \land n = w \land p = i) \land q = v) \to k = U$
17	15 16	cbvrexdva2	$⊢ ((k = U \land l = z \land m = f) \land n = w \land p = i) \to (\exists q \in k (p \in q \land q \in m) \leftrightarrow \exists v \in U (i \in v \land v \in f))$
18		simpl3	$⊢ (((k = U \land l = z \land m = f) \land n = w \land p = i) \land r = u) \to p = i$
19		simpr	$⊢ (((k = U \land l = z \land m = f) \land n = w \land p = i) \land r = u) \to r = u$
20	18 19	eleq12d	$⊢ (((k = U \land l = z \land m = f) \land n = w \land p = i) \land r = u) \to (p \in r \leftrightarrow i \in u)$
21	19	unieqd	$⊢ (((k = U \land l = z \land m = f) \land n = w \land p = i) \land r = u) \to ⋃ r = ⋃ u$
22		simpl2	$⊢ (((k = U \land l = z \land m = f) \land n = w \land p = i) \land r = u) \to n = w$
23	21 22	sseq12d	$⊢ (((k = U \land l = z \land m = f) \land n = w \land p = i) \land r = u) \to (⋃ r \subseteq n \leftrightarrow ⋃ u \subseteq w)$
24	20 23	anbi12d	$⊢ (((k = U \land l = z \land m = f) \land n = w \land p = i) \land r = u) \to ((p \in r \land ⋃ r \subseteq n) \leftrightarrow (i \in u \land ⋃ u \subseteq w))$
25		simpl13	$⊢ (((k = U \land l = z \land m = f) \land n = w \land p = i) \land r = u) \to m = f$
26	24 25	cbvrexdva2	$⊢ ((k = U \land l = z \land m = f) \land n = w \land p = i) \to (\exists r \in m (p \in r \land ⋃ r \subseteq n) \leftrightarrow \exists u \in f (i \in u \land ⋃ u \subseteq w))$
27	17 26	imbi12d	$⊢ ((k = U \land l = z \land m = f) \land n = w \land p = i) \to ((\exists q \in k (p \in q \land q \in m) \to \exists r \in m (p \in r \land ⋃ r \subseteq n)) \leftrightarrow (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))$
28	27	3expa	$⊢ (((k = U \land l = z \land m = f) \land n = w) \land p = i) \to ((\exists q \in k (p \in q \land q \in m) \to \exists r \in m (p \in r \land ⋃ r \subseteq n)) \leftrightarrow (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))$
29		simpll2	$⊢ (((k = U \land l = z \land m = f) \land n = w) \land p = i) \to l = z$
30	28 29	cbvraldva2	$⊢ ((k = U \land l = z \land m = f) \land n = w) \to (\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)) \leftrightarrow \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))$
31	9 30	anbi12d	$⊢ ((k = U \land l = z \land m = f) \land n = w) \to ((𝒫 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))) \leftrightarrow (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))))$
32		simpl1	$⊢ ((k = U \land l = z \land m = f) \land n = w) \to k = U$
33	31 32	cbvrexdva2	$⊢ (k = U \land l = z \land m = f) \to (\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))) \leftrightarrow \exists w \in U (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))))$
34	33	3expa	$⊢ ((k = U \land l = z) \land m = f) \to (\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))) \leftrightarrow \exists w \in U (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))))$
35	34	cbvaldvaw	$⊢ (k = U \land l = z) \to (\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))) \leftrightarrow \forall f \exists w \in U (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w))))$
36	5 35	anbi12d	$⊢ (k = U \land l = z) \to ((𝒫 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)))) \leftrightarrow (𝒫 z \subseteq U \land \forall f \exists w \in U (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))))$
37	36 4	cbvraldva2	$⊢ k = U \to (\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)))) \leftrightarrow \forall z \in U (𝒫 z \subseteq U \land \forall f \exists w \in U (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))))$
38	37 1	elab2g	$⊢ U \in V \to (U \in M \leftrightarrow \forall z \in U (𝒫 z \subseteq U \land \forall f \exists w \in U (𝒫 z \subseteq w \land \forall i \in z (\exists v \in U (i \in v \land v \in f) \to \exists u \in f (i \in u \land ⋃ u \subseteq w)))))$

Metamath Proof Explorer

Theorem ismnu

Proof