Theorem ismnu 44230

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

A minimal universe is closed under subsets (mnussd 44232), powersets (mnupwd 44236), and an operation which is similar to a combination of collection and union (mnuop3d 44240), from which closure under pairing (mnuprd 44245), unions (mnuunid 44246), and function ranges (mnurnd 44252) can be deduced, from which equivalence with Grothendieck universes (grumnueq 44256) 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 484	. . . . . 6 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → 𝑙 = 𝑧)
2	1	pweqd 4639	. . . . 5 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → 𝒫 𝑙 = 𝒫 𝑧)
3		simpl 482	. . . . 5 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → 𝑘 = 𝑈)
4	2, 3	sseq12d 4042	. . . 4 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → (𝒫 𝑙 ⊆ 𝑘 ↔ 𝒫 𝑧 ⊆ 𝑈))
5	2	3adant3 1132	. . . . . . . . . 10 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) → 𝒫 𝑙 = 𝒫 𝑧)
6	5	adantr 480	. . . . . . . . 9 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝒫 𝑙 = 𝒫 𝑧)
7		simpr 484	. . . . . . . . 9 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝑛 = 𝑤)
8	6, 7	sseq12d 4042	. . . . . . . 8 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → (𝒫 𝑙 ⊆ 𝑛 ↔ 𝒫 𝑧 ⊆ 𝑤))
9		simpl3 1193	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑝 = 𝑖)
10		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑞 = 𝑣)
11	9, 10	eleq12d 2838	. . . . . . . . . . . . 13 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → (𝑝 ∈ 𝑞 ↔ 𝑖 ∈ 𝑣))
12		simpl13 1250	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑚 = 𝑓)
13	10, 12	eleq12d 2838	. . . . . . . . . . . . 13 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → (𝑞 ∈ 𝑚 ↔ 𝑣 ∈ 𝑓))
14	11, 13	anbi12d 631	. . . . . . . . . . . 12 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → ((𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) ↔ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
15		simpl11 1248	. . . . . . . . . . . 12 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑘 = 𝑈)
16	14, 15	cbvrexdva2 3357	. . . . . . . . . . 11 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) → (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) ↔ ∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
17		simpl3 1193	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑝 = 𝑖)
18		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑟 = 𝑢)
19	17, 18	eleq12d 2838	. . . . . . . . . . . . 13 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → (𝑝 ∈ 𝑟 ↔ 𝑖 ∈ 𝑢))
20	18	unieqd 4944	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → ∪ 𝑟 = ∪ 𝑢)
21		simpl2 1192	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑛 = 𝑤)
22	20, 21	sseq12d 4042	. . . . . . . . . . . . 13 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → (∪ 𝑟 ⊆ 𝑛 ↔ ∪ 𝑢 ⊆ 𝑤))
23	19, 22	anbi12d 631	. . . . . . . . . . . 12 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → ((𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛) ↔ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
24		simpl13 1250	. . . . . . . . . . . 12 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑚 = 𝑓)
25	23, 24	cbvrexdva2 3357	. . . . . . . . . . 11 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) → (∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛) ↔ ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
26	16, 25	imbi12d 344	. . . . . . . . . 10 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) → ((∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)) ↔ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
27	26	3expa 1118	. . . . . . . . 9 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) ∧ 𝑝 = 𝑖) → ((∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)) ↔ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
28		simpll2 1213	. . . . . . . . 9 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) ∧ 𝑝 = 𝑖) → 𝑙 = 𝑧)
29	27, 28	cbvraldva2 3356	. . . . . . . 8 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → (∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)) ↔ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
30	8, 29	anbi12d 631	. . . . . . 7 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → ((𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))) ↔ (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
31		simpl1 1191	. . . . . . 7 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝑘 = 𝑈)
32	30, 31	cbvrexdva2 3357	. . . . . 6 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) → (∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))) ↔ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
33	32	3expa 1118	. . . . 5 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) ∧ 𝑚 = 𝑓) → (∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))) ↔ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
34	33	cbvaldvaw 2037	. . . 4 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → (∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))) ↔ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
35	4, 34	anbi12d 631	. . 3 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → ((𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)))) ↔ (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))))
36	35, 3	cbvraldva2 3356	. 2 ⊢ (𝑘 = 𝑈 → (∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)))) ↔ ∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))))
37		ismnu.1	. 2 ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}
38	36, 37	elab2g 3696	1 ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ 𝑀 ↔ ∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087  ∀wal 1535   = wceq 1537   ∈ wcel 2108  {cab 2717  ∀wral 3067  ∃wrex 3076   ⊆ wss 3976  𝒫 cpw 4622  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-v 3490  df-ss 3993  df-pw 4624  df-uni 4932

This theorem is referenced by:  mnuop123d  44231  grumnudlem  44254  rr-grothprimbi  44264  rr-groth  44268  dfuniv2  44271