Theorem ismnu 45339

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 45365 to be exactly Grothendicek universes. Minimal universes are sets which satisfy the predicate on 𝑦 in rr-groth 45377, except for the 𝑥 ∈ 𝑦 clause.

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

Hypothesis

Ref	Expression
ismnu.1	⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}

Assertion

Ref	Expression
ismnu	⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ 𝑀 ↔ ∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))))

Distinct variable groups:   𝑧,𝑤,𝑣,𝑈,𝑓,𝑖,𝑘,𝑚,𝑛,𝑞,𝑝,𝑙   𝑧,𝑢,𝑟,𝑤,𝑈,𝑓,𝑖,𝑘,𝑚,𝑛,𝑝,𝑙

Allowed substitution hints:   𝑀(𝑧, 𝑤, 𝑣, 𝑢, 𝑓, 𝑖, 𝑘, 𝑚, 𝑛, 𝑟, 𝑞, 𝑝, 𝑙)   𝑉(𝑧, 𝑤, 𝑣, 𝑢, 𝑓, 𝑖, 𝑘, 𝑚, 𝑛, 𝑟, 𝑞, 𝑝, 𝑙)

Proof of Theorem ismnu

Step	Hyp	Ref	Expression
1		simpr 490	. . . . . 6 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → 𝑙 = 𝑧)
2	1	pweqd 4573	. . . . 5 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → 𝒫 𝑙 = 𝒫 𝑧)
3		simpl 488	. . . . 5 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → 𝑘 = 𝑈)
4	2, 3	sseq12d 3941	. . . 4 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → (𝒫 𝑙 ⊆ 𝑘 ↔ 𝒫 𝑧 ⊆ 𝑈))
5	2	3adant3 1150	. . . . . . . . . 10 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) → 𝒫 𝑙 = 𝒫 𝑧)
6	5	adantr 486	. . . . . . . . 9 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝒫 𝑙 = 𝒫 𝑧)
7		simpr 490	. . . . . . . . 9 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝑛 = 𝑤)
8	6, 7	sseq12d 3941	. . . . . . . 8 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → (𝒫 𝑙 ⊆ 𝑛 ↔ 𝒫 𝑧 ⊆ 𝑤))
9		simpl3 1212	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑝 = 𝑖)
10		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑞 = 𝑣)
11	9, 10	eleq12d 2854	. . . . . . . . . . . . 13 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → (𝑝 ∈ 𝑞 ↔ 𝑖 ∈ 𝑣))
12		simpl13 1269	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑚 = 𝑓)
13	10, 12	eleq12d 2854	. . . . . . . . . . . . 13 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → (𝑞 ∈ 𝑚 ↔ 𝑣 ∈ 𝑓))
14	11, 13	anbi12d 644	. . . . . . . . . . . 12 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → ((𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) ↔ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
15		simpl11 1267	. . . . . . . . . . . 12 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑘 = 𝑈)
16	14, 15	cbvrexdva2 3337	. . . . . . . . . . 11 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) → (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) ↔ ∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
17		simpl3 1212	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑝 = 𝑖)
18		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑟 = 𝑢)
19	17, 18	eleq12d 2854	. . . . . . . . . . . . 13 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → (𝑝 ∈ 𝑟 ↔ 𝑖 ∈ 𝑢))
20	18	unieqd 4879	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → ∪ 𝑟 = ∪ 𝑢)
21		simpl2 1211	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑛 = 𝑤)
22	20, 21	sseq12d 3941	. . . . . . . . . . . . 13 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → (∪ 𝑟 ⊆ 𝑛 ↔ ∪ 𝑢 ⊆ 𝑤))
23	19, 22	anbi12d 644	. . . . . . . . . . . 12 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → ((𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛) ↔ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
24		simpl13 1269	. . . . . . . . . . . 12 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑚 = 𝑓)
25	23, 24	cbvrexdva2 3337	. . . . . . . . . . 11 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) → (∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛) ↔ ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
26	16, 25	imbi12d 347	. . . . . . . . . 10 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) → ((∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)) ↔ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
27	26	3expa 1136	. . . . . . . . 9 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) ∧ 𝑝 = 𝑖) → ((∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)) ↔ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
28		simpll2 1232	. . . . . . . . 9 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) ∧ 𝑝 = 𝑖) → 𝑙 = 𝑧)
29	27, 28	cbvraldva2 3336	. . . . . . . 8 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → (∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)) ↔ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
30	8, 29	anbi12d 644	. . . . . . 7 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → ((𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))) ↔ (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
31		simpl1 1210	. . . . . . 7 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝑘 = 𝑈)
32	30, 31	cbvrexdva2 3337	. . . . . 6 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) → (∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))) ↔ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
33	32	3expa 1136	. . . . 5 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) ∧ 𝑚 = 𝑓) → (∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))) ↔ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
34	33	cbvaldvaw 2070	. . . 4 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → (∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))) ↔ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
35	4, 34	anbi12d 644	. . 3 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → ((𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)))) ↔ (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))))
36	35, 3	cbvraldva2 3336	. 2 ⊢ (𝑘 = 𝑈 → (∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)))) ↔ ∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))))
37		ismnu.1	. 2 ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}
38	36, 37	elab2g 3633	1 ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ 𝑀 ↔ ∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103  ∀wal 1567   = wceq 1569   ∈ wcel 2144  {cab 2738  ∀wral 3076  ∃wrex 3086   ⊆ wss 3895  𝒫 cpw 4556  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-v 3452  df-ss 3896  df-pw 4558  df-uni 4867

This theorem is used by:  mnuop123d  45340  grumnudlem  45363  rr-grothprimbi  45373  rr-groth  45377  dfuniv2  45380