Theorem ismnu 45093

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

A minimal universe is closed under subsets (mnussd 45095), powersets (mnupwd 45099), and an operation which is similar to a combination of collection and union (mnuop3d 45103), from which closure under pairing (mnuprd 45108), unions (mnuunid 45109), and function ranges (mnurnd 45115) can be deduced, from which equivalence with Grothendieck universes (grumnueq 45119) 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 4577	. . . . 5 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → 𝒫 𝑙 = 𝒫 𝑧)
3		simpl 488	. . . . 5 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → 𝑘 = 𝑈)
4	2, 3	sseq12d 3967	. . . 4 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → (𝒫 𝑙 ⊆ 𝑘 ↔ 𝒫 𝑧 ⊆ 𝑈))
5	2	3adant3 1150	. . . . . . . . . 10 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) → 𝒫 𝑙 = 𝒫 𝑧)
6	5	adantr 486	. . . . . . . . 9 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝒫 𝑙 = 𝒫 𝑧)
7		simpr 490	. . . . . . . . 9 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝑛 = 𝑤)
8	6, 7	sseq12d 3967	. . . . . . . 8 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → (𝒫 𝑙 ⊆ 𝑛 ↔ 𝒫 𝑧 ⊆ 𝑤))
9		simpl3 1212	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑝 = 𝑖)
10		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑞 = 𝑣)
11	9, 10	eleq12d 2856	. . . . . . . . . . . . 13 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → (𝑝 ∈ 𝑞 ↔ 𝑖 ∈ 𝑣))
12		simpl13 1269	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑚 = 𝑓)
13	10, 12	eleq12d 2856	. . . . . . . . . . . . 13 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → (𝑞 ∈ 𝑚 ↔ 𝑣 ∈ 𝑓))
14	11, 13	anbi12d 644	. . . . . . . . . . . 12 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → ((𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) ↔ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
15		simpl11 1267	. . . . . . . . . . . 12 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑘 = 𝑈)
16	14, 15	cbvrexdva2 3339	. . . . . . . . . . 11 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) → (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) ↔ ∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
17		simpl3 1212	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑝 = 𝑖)
18		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑟 = 𝑢)
19	17, 18	eleq12d 2856	. . . . . . . . . . . . 13 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → (𝑝 ∈ 𝑟 ↔ 𝑖 ∈ 𝑢))
20	18	unieqd 4883	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → ∪ 𝑟 = ∪ 𝑢)
21		simpl2 1211	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑛 = 𝑤)
22	20, 21	sseq12d 3967	. . . . . . . . . . . . 13 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → (∪ 𝑟 ⊆ 𝑛 ↔ ∪ 𝑢 ⊆ 𝑤))
23	19, 22	anbi12d 644	. . . . . . . . . . . 12 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → ((𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛) ↔ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
24		simpl13 1269	. . . . . . . . . . . 12 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑚 = 𝑓)
25	23, 24	cbvrexdva2 3339	. . . . . . . . . . 11 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) → (∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛) ↔ ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
26	16, 25	imbi12d 347	. . . . . . . . . 10 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) → ((∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)) ↔ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
27	26	3expa 1136	. . . . . . . . 9 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) ∧ 𝑝 = 𝑖) → ((∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)) ↔ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
28		simpll2 1232	. . . . . . . . 9 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) ∧ 𝑝 = 𝑖) → 𝑙 = 𝑧)
29	27, 28	cbvraldva2 3338	. . . . . . . 8 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → (∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)) ↔ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
30	8, 29	anbi12d 644	. . . . . . 7 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → ((𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))) ↔ (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
31		simpl1 1210	. . . . . . 7 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝑘 = 𝑈)
32	30, 31	cbvrexdva2 3339	. . . . . 6 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) → (∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))) ↔ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
33	32	3expa 1136	. . . . 5 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) ∧ 𝑚 = 𝑓) → (∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))) ↔ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
34	33	cbvaldvaw 2071	. . . 4 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → (∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))) ↔ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
35	4, 34	anbi12d 644	. . 3 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → ((𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)))) ↔ (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))))
36	35, 3	cbvraldva2 3338	. 2 ⊢ (𝑘 = 𝑈 → (∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)))) ↔ ∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))))
37		ismnu.1	. 2 ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}
38	36, 37	elab2g 3637	1 ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ 𝑀 ↔ ∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103  ∀wal 1568   = wceq 1570   ∈ wcel 2145  {cab 2740  ∀wral 3078  ∃wrex 3088   ⊆ wss 3902  𝒫 cpw 4560  ∪ cuni 4870

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-v 3455  df-ss 3919  df-pw 4562  df-uni 4871

This theorem is used by:  mnuop123d  45094  grumnudlem  45117  rr-grothprimbi  45127  rr-groth  45131  dfuniv2  45134