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

A minimal universe is closed under subsets (mnussd 43571), powersets (mnupwd 43575), and an operation which is similar to a combination of collection and union (mnuop3d 43579), from which closure under pairing (mnuprd 43584), unions (mnuunid 43585), and function ranges (mnurnd 43591) can be deduced, from which equivalence with Grothendieck universes (grumnueq 43595) 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 4612 . . . . 5 ((𝑘 = 𝑈𝑙 = 𝑧) → 𝒫 𝑙 = 𝒫 𝑧)
3 simpl 482 . . . . 5 ((𝑘 = 𝑈𝑙 = 𝑧) → 𝑘 = 𝑈)
42, 3sseq12d 4008 . . . 4 ((𝑘 = 𝑈𝑙 = 𝑧) → (𝒫 𝑙𝑘 ↔ 𝒫 𝑧𝑈))
523adant3 1129 . . . . . . . . . 10 ((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) → 𝒫 𝑙 = 𝒫 𝑧)
65adantr 480 . . . . . . . . 9 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝒫 𝑙 = 𝒫 𝑧)
7 simpr 484 . . . . . . . . 9 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝑛 = 𝑤)
86, 7sseq12d 4008 . . . . . . . 8 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → (𝒫 𝑙𝑛 ↔ 𝒫 𝑧𝑤))
9 simpl3 1190 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑝 = 𝑖)
10 simpr 484 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑞 = 𝑣)
119, 10eleq12d 2819 . . . . . . . . . . . . 13 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → (𝑝𝑞𝑖𝑣))
12 simpl13 1247 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑚 = 𝑓)
1310, 12eleq12d 2819 . . . . . . . . . . . . 13 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → (𝑞𝑚𝑣𝑓))
1411, 13anbi12d 630 . . . . . . . . . . . 12 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → ((𝑝𝑞𝑞𝑚) ↔ (𝑖𝑣𝑣𝑓)))
15 simpl11 1245 . . . . . . . . . . . 12 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑘 = 𝑈)
1614, 15cbvrexdva2 3337 . . . . . . . . . . 11 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) → (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) ↔ ∃𝑣𝑈 (𝑖𝑣𝑣𝑓)))
17 simpl3 1190 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑝 = 𝑖)
18 simpr 484 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑟 = 𝑢)
1917, 18eleq12d 2819 . . . . . . . . . . . . 13 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → (𝑝𝑟𝑖𝑢))
2018unieqd 4913 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑟 = 𝑢)
21 simpl2 1189 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑛 = 𝑤)
2220, 21sseq12d 4008 . . . . . . . . . . . . 13 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → ( 𝑟𝑛 𝑢𝑤))
2319, 22anbi12d 630 . . . . . . . . . . . 12 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → ((𝑝𝑟 𝑟𝑛) ↔ (𝑖𝑢 𝑢𝑤)))
24 simpl13 1247 . . . . . . . . . . . 12 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑚 = 𝑓)
2523, 24cbvrexdva2 3337 . . . . . . . . . . 11 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) → (∃𝑟𝑚 (𝑝𝑟 𝑟𝑛) ↔ ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
2616, 25imbi12d 344 . . . . . . . . . 10 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) → ((∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)) ↔ (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
27263expa 1115 . . . . . . . . 9 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) ∧ 𝑝 = 𝑖) → ((∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)) ↔ (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
28 simpll2 1210 . . . . . . . . 9 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) ∧ 𝑝 = 𝑖) → 𝑙 = 𝑧)
2927, 28cbvraldva2 3336 . . . . . . . 8 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → (∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)) ↔ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
308, 29anbi12d 630 . . . . . . 7 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → ((𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))) ↔ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
31 simpl1 1188 . . . . . . 7 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝑘 = 𝑈)
3230, 31cbvrexdva2 3337 . . . . . 6 ((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) → (∃𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))) ↔ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
33323expa 1115 . . . . 5 (((𝑘 = 𝑈𝑙 = 𝑧) ∧ 𝑚 = 𝑓) → (∃𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))) ↔ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
3433cbvaldvaw 2033 . . . 4 ((𝑘 = 𝑈𝑙 = 𝑧) → (∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))) ↔ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
354, 34anbi12d 630 . . 3 ((𝑘 = 𝑈𝑙 = 𝑧) → ((𝒫 𝑙𝑘 ∧ ∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)))) ↔ (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))))
3635, 3cbvraldva2 3336 . 2 (𝑘 = 𝑈 → (∀𝑙𝑘 (𝒫 𝑙𝑘 ∧ ∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)))) ↔ ∀𝑧𝑈 (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))))
37 ismnu.1 . 2 𝑀 = {𝑘 ∣ ∀𝑙𝑘 (𝒫 𝑙𝑘 ∧ ∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))))}
3836, 37elab2g 3663 1 (𝑈𝑉 → (𝑈𝑀 ↔ ∀𝑧𝑈 (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1084  wal 1531   = wceq 1533  wcel 2098  {cab 2701  wral 3053  wrex 3062  wss 3941  𝒫 cpw 4595   cuni 4900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695
This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1086  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ral 3054  df-rex 3063  df-v 3468  df-in 3948  df-ss 3958  df-pw 4597  df-uni 4901
This theorem is referenced by:  mnuop123d  43570  grumnudlem  43593  rr-grothprimbi  43603  rr-groth  43607  dfuniv2  43610
  Copyright terms: Public domain W3C validator