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

A minimal universe is closed under subsets (mnussd 42533), powersets (mnupwd 42537), and an operation which is similar to a combination of collection and union (mnuop3d 42541), from which closure under pairing (mnuprd 42546), unions (mnuunid 42547), and function ranges (mnurnd 42553) can be deduced, from which equivalence with Grothendieck universes (grumnueq 42557) 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 485 . . . . . 6 ((𝑘 = 𝑈𝑙 = 𝑧) → 𝑙 = 𝑧)
21pweqd 4577 . . . . 5 ((𝑘 = 𝑈𝑙 = 𝑧) → 𝒫 𝑙 = 𝒫 𝑧)
3 simpl 483 . . . . 5 ((𝑘 = 𝑈𝑙 = 𝑧) → 𝑘 = 𝑈)
42, 3sseq12d 3977 . . . 4 ((𝑘 = 𝑈𝑙 = 𝑧) → (𝒫 𝑙𝑘 ↔ 𝒫 𝑧𝑈))
523adant3 1132 . . . . . . . . . 10 ((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) → 𝒫 𝑙 = 𝒫 𝑧)
65adantr 481 . . . . . . . . 9 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝒫 𝑙 = 𝒫 𝑧)
7 simpr 485 . . . . . . . . 9 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝑛 = 𝑤)
86, 7sseq12d 3977 . . . . . . . 8 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → (𝒫 𝑙𝑛 ↔ 𝒫 𝑧𝑤))
9 simpl3 1193 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑝 = 𝑖)
10 simpr 485 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑞 = 𝑣)
119, 10eleq12d 2832 . . . . . . . . . . . . 13 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → (𝑝𝑞𝑖𝑣))
12 simpl13 1250 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑚 = 𝑓)
1310, 12eleq12d 2832 . . . . . . . . . . . . 13 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → (𝑞𝑚𝑣𝑓))
1411, 13anbi12d 631 . . . . . . . . . . . 12 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → ((𝑝𝑞𝑞𝑚) ↔ (𝑖𝑣𝑣𝑓)))
15 simpl11 1248 . . . . . . . . . . . 12 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑘 = 𝑈)
1614, 15cbvrexdva2 3324 . . . . . . . . . . 11 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) → (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) ↔ ∃𝑣𝑈 (𝑖𝑣𝑣𝑓)))
17 simpl3 1193 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑝 = 𝑖)
18 simpr 485 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑟 = 𝑢)
1917, 18eleq12d 2832 . . . . . . . . . . . . 13 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → (𝑝𝑟𝑖𝑢))
2018unieqd 4879 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑟 = 𝑢)
21 simpl2 1192 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑛 = 𝑤)
2220, 21sseq12d 3977 . . . . . . . . . . . . 13 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → ( 𝑟𝑛 𝑢𝑤))
2319, 22anbi12d 631 . . . . . . . . . . . 12 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → ((𝑝𝑟 𝑟𝑛) ↔ (𝑖𝑢 𝑢𝑤)))
24 simpl13 1250 . . . . . . . . . . . 12 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑚 = 𝑓)
2523, 24cbvrexdva2 3324 . . . . . . . . . . 11 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) → (∃𝑟𝑚 (𝑝𝑟 𝑟𝑛) ↔ ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
2616, 25imbi12d 344 . . . . . . . . . 10 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) → ((∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)) ↔ (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
27263expa 1118 . . . . . . . . 9 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) ∧ 𝑝 = 𝑖) → ((∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)) ↔ (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
28 simpll2 1213 . . . . . . . . 9 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) ∧ 𝑝 = 𝑖) → 𝑙 = 𝑧)
2927, 28cbvraldva2 3323 . . . . . . . 8 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → (∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)) ↔ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
308, 29anbi12d 631 . . . . . . 7 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → ((𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))) ↔ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
31 simpl1 1191 . . . . . . 7 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝑘 = 𝑈)
3230, 31cbvrexdva2 3324 . . . . . 6 ((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) → (∃𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))) ↔ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
33323expa 1118 . . . . 5 (((𝑘 = 𝑈𝑙 = 𝑧) ∧ 𝑚 = 𝑓) → (∃𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))) ↔ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
3433cbvaldvaw 2041 . . . 4 ((𝑘 = 𝑈𝑙 = 𝑧) → (∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))) ↔ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
354, 34anbi12d 631 . . 3 ((𝑘 = 𝑈𝑙 = 𝑧) → ((𝒫 𝑙𝑘 ∧ ∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)))) ↔ (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))))
3635, 3cbvraldva2 3323 . 2 (𝑘 = 𝑈 → (∀𝑙𝑘 (𝒫 𝑙𝑘 ∧ ∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)))) ↔ ∀𝑧𝑈 (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))))
37 ismnu.1 . 2 𝑀 = {𝑘 ∣ ∀𝑙𝑘 (𝒫 𝑙𝑘 ∧ ∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))))}
3836, 37elab2g 3632 1 (𝑈𝑉 → (𝑈𝑀 ↔ ∀𝑧𝑈 (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087  wal 1539   = wceq 1541  wcel 2106  {cab 2713  wral 3064  wrex 3073  wss 3910  𝒫 cpw 4560   cuni 4865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1089  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3065  df-rex 3074  df-v 3447  df-in 3917  df-ss 3927  df-pw 4562  df-uni 4866
This theorem is referenced by:  mnuop123d  42532  grumnudlem  42555  rr-grothprimbi  42565  rr-groth  42569  dfuniv2  42572
  Copyright terms: Public domain W3C validator