Users' Mathboxes Mathbox for Rohan Ridenour < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ismnu Structured version   Visualization version   GIF version

Theorem ismnu 43482
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 43508 to be exactly Grothendicek universes. Minimal universes are sets which satisfy the predicate on 𝑦 in rr-groth 43520, except for the 𝑥𝑦 clause.

A minimal universe is closed under subsets (mnussd 43484), powersets (mnupwd 43488), and an operation which is similar to a combination of collection and union (mnuop3d 43492), from which closure under pairing (mnuprd 43497), unions (mnuunid 43498), and function ranges (mnurnd 43504) can be deduced, from which equivalence with Grothendieck universes (grumnueq 43508) 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
StepHypRef Expression
1 simpr 484 . . . . . 6 ((𝑘 = 𝑈𝑙 = 𝑧) → 𝑙 = 𝑧)
21pweqd 4619 . . . . 5 ((𝑘 = 𝑈𝑙 = 𝑧) → 𝒫 𝑙 = 𝒫 𝑧)
3 simpl 482 . . . . 5 ((𝑘 = 𝑈𝑙 = 𝑧) → 𝑘 = 𝑈)
42, 3sseq12d 4015 . . . 4 ((𝑘 = 𝑈𝑙 = 𝑧) → (𝒫 𝑙𝑘 ↔ 𝒫 𝑧𝑈))
523adant3 1131 . . . . . . . . . 10 ((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) → 𝒫 𝑙 = 𝒫 𝑧)
65adantr 480 . . . . . . . . 9 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝒫 𝑙 = 𝒫 𝑧)
7 simpr 484 . . . . . . . . 9 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝑛 = 𝑤)
86, 7sseq12d 4015 . . . . . . . 8 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → (𝒫 𝑙𝑛 ↔ 𝒫 𝑧𝑤))
9 simpl3 1192 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑝 = 𝑖)
10 simpr 484 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑞 = 𝑣)
119, 10eleq12d 2826 . . . . . . . . . . . . 13 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → (𝑝𝑞𝑖𝑣))
12 simpl13 1249 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑚 = 𝑓)
1310, 12eleq12d 2826 . . . . . . . . . . . . 13 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → (𝑞𝑚𝑣𝑓))
1411, 13anbi12d 630 . . . . . . . . . . . 12 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → ((𝑝𝑞𝑞𝑚) ↔ (𝑖𝑣𝑣𝑓)))
15 simpl11 1247 . . . . . . . . . . . 12 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑘 = 𝑈)
1614, 15cbvrexdva2 3344 . . . . . . . . . . 11 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) → (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) ↔ ∃𝑣𝑈 (𝑖𝑣𝑣𝑓)))
17 simpl3 1192 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑝 = 𝑖)
18 simpr 484 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑟 = 𝑢)
1917, 18eleq12d 2826 . . . . . . . . . . . . 13 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → (𝑝𝑟𝑖𝑢))
2018unieqd 4922 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑟 = 𝑢)
21 simpl2 1191 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑛 = 𝑤)
2220, 21sseq12d 4015 . . . . . . . . . . . . 13 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → ( 𝑟𝑛 𝑢𝑤))
2319, 22anbi12d 630 . . . . . . . . . . . 12 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → ((𝑝𝑟 𝑟𝑛) ↔ (𝑖𝑢 𝑢𝑤)))
24 simpl13 1249 . . . . . . . . . . . 12 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑚 = 𝑓)
2523, 24cbvrexdva2 3344 . . . . . . . . . . 11 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) → (∃𝑟𝑚 (𝑝𝑟 𝑟𝑛) ↔ ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
2616, 25imbi12d 344 . . . . . . . . . 10 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) → ((∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)) ↔ (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
27263expa 1117 . . . . . . . . 9 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) ∧ 𝑝 = 𝑖) → ((∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)) ↔ (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
28 simpll2 1212 . . . . . . . . 9 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) ∧ 𝑝 = 𝑖) → 𝑙 = 𝑧)
2927, 28cbvraldva2 3343 . . . . . . . 8 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → (∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)) ↔ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
308, 29anbi12d 630 . . . . . . 7 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → ((𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))) ↔ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
31 simpl1 1190 . . . . . . 7 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝑘 = 𝑈)
3230, 31cbvrexdva2 3344 . . . . . 6 ((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) → (∃𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))) ↔ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
33323expa 1117 . . . . 5 (((𝑘 = 𝑈𝑙 = 𝑧) ∧ 𝑚 = 𝑓) → (∃𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))) ↔ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
3433cbvaldvaw 2040 . . . 4 ((𝑘 = 𝑈𝑙 = 𝑧) → (∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))) ↔ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
354, 34anbi12d 630 . . 3 ((𝑘 = 𝑈𝑙 = 𝑧) → ((𝒫 𝑙𝑘 ∧ ∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)))) ↔ (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))))
3635, 3cbvraldva2 3343 . 2 (𝑘 = 𝑈 → (∀𝑙𝑘 (𝒫 𝑙𝑘 ∧ ∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)))) ↔ ∀𝑧𝑈 (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))))
37 ismnu.1 . 2 𝑀 = {𝑘 ∣ ∀𝑙𝑘 (𝒫 𝑙𝑘 ∧ ∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))))}
3836, 37elab2g 3670 1 (𝑈𝑉 → (𝑈𝑀 ↔ ∀𝑧𝑈 (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1086  wal 1538   = wceq 1540  wcel 2105  {cab 2708  wral 3060  wrex 3069  wss 3948  𝒫 cpw 4602   cuni 4908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1088  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-v 3475  df-in 3955  df-ss 3965  df-pw 4604  df-uni 4909
This theorem is referenced by:  mnuop123d  43483  grumnudlem  43506  rr-grothprimbi  43516  rr-groth  43520  dfuniv2  43523
  Copyright terms: Public domain W3C validator