Theorem ismnu 44797

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

A minimal universe is closed under subsets (mnussd 44799), powersets (mnupwd 44803), and an operation which is similar to a combination of collection and union (mnuop3d 44807), from which closure under pairing (mnuprd 44812), unions (mnuunid 44813), and function ranges (mnurnd 44819) can be deduced, from which equivalence with Grothendieck universes (grumnueq 44823) 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 488	. . . . . 6 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → 𝑙 = 𝑧)
2	1	pweqd 4569	. . . . 5 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → 𝒫 𝑙 = 𝒫 𝑧)
3		simpl 486	. . . . 5 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → 𝑘 = 𝑈)
4	2, 3	sseq12d 3967	. . . 4 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → (𝒫 𝑙 ⊆ 𝑘 ↔ 𝒫 𝑧 ⊆ 𝑈))
5	2	3adant3 1144	. . . . . . . . . 10 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) → 𝒫 𝑙 = 𝒫 𝑧)
6	5	adantr 484	. . . . . . . . 9 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝒫 𝑙 = 𝒫 𝑧)
7		simpr 488	. . . . . . . . 9 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝑛 = 𝑤)
8	6, 7	sseq12d 3967	. . . . . . . 8 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → (𝒫 𝑙 ⊆ 𝑛 ↔ 𝒫 𝑧 ⊆ 𝑤))
9		simpl3 1206	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑝 = 𝑖)
10		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑞 = 𝑣)
11	9, 10	eleq12d 2855	. . . . . . . . . . . . 13 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → (𝑝 ∈ 𝑞 ↔ 𝑖 ∈ 𝑣))
12		simpl13 1263	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑚 = 𝑓)
13	10, 12	eleq12d 2855	. . . . . . . . . . . . 13 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → (𝑞 ∈ 𝑚 ↔ 𝑣 ∈ 𝑓))
14	11, 13	anbi12d 641	. . . . . . . . . . . 12 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → ((𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) ↔ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
15		simpl11 1261	. . . . . . . . . . . 12 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑘 = 𝑈)
16	14, 15	cbvrexdva2 3338	. . . . . . . . . . 11 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) → (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) ↔ ∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)))
17		simpl3 1206	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑝 = 𝑖)
18		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑟 = 𝑢)
19	17, 18	eleq12d 2855	. . . . . . . . . . . . 13 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → (𝑝 ∈ 𝑟 ↔ 𝑖 ∈ 𝑢))
20	18	unieqd 4875	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → ∪ 𝑟 = ∪ 𝑢)
21		simpl2 1205	. . . . . . . . . . . . . 14 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑛 = 𝑤)
22	20, 21	sseq12d 3967	. . . . . . . . . . . . 13 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → (∪ 𝑟 ⊆ 𝑛 ↔ ∪ 𝑢 ⊆ 𝑤))
23	19, 22	anbi12d 641	. . . . . . . . . . . 12 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → ((𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛) ↔ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
24		simpl13 1263	. . . . . . . . . . . 12 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑚 = 𝑓)
25	23, 24	cbvrexdva2 3338	. . . . . . . . . . 11 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) → (∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛) ↔ ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
26	16, 25	imbi12d 346	. . . . . . . . . 10 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤 ∧ 𝑝 = 𝑖) → ((∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)) ↔ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
27	26	3expa 1130	. . . . . . . . 9 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) ∧ 𝑝 = 𝑖) → ((∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)) ↔ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
28		simpll2 1226	. . . . . . . . 9 ⊢ ((((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) ∧ 𝑝 = 𝑖) → 𝑙 = 𝑧)
29	27, 28	cbvraldva2 3337	. . . . . . . 8 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → (∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)) ↔ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
30	8, 29	anbi12d 641	. . . . . . 7 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → ((𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))) ↔ (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
31		simpl1 1204	. . . . . . 7 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝑘 = 𝑈)
32	30, 31	cbvrexdva2 3338	. . . . . 6 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧 ∧ 𝑚 = 𝑓) → (∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))) ↔ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
33	32	3expa 1130	. . . . 5 ⊢ (((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) ∧ 𝑚 = 𝑓) → (∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))) ↔ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
34	33	cbvaldvaw 2057	. . . 4 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → (∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))) ↔ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))))
35	4, 34	anbi12d 641	. . 3 ⊢ ((𝑘 = 𝑈 ∧ 𝑙 = 𝑧) → ((𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)))) ↔ (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))))
36	35, 3	cbvraldva2 3337	. 2 ⊢ (𝑘 = 𝑈 → (∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛)))) ↔ ∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))))
37		ismnu.1	. 2 ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}
38	36, 37	elab2g 3638	1 ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ 𝑀 ↔ ∀𝑧 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1097  ∀wal 1557   = wceq 1559   ∈ wcel 2141  {cab 2739  ∀wral 3075  ∃wrex 3085   ⊆ wss 3902  𝒫 cpw 4552  ∪ cuni 4862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1099  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-v 3455  df-ss 3919  df-pw 4554  df-uni 4863

This theorem is referenced by:  mnuop123d  44798  grumnudlem  44821  rr-grothprimbi  44831  rr-groth  44835  dfuniv2  44838