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

A minimal universe is closed under subsets (mnussd 41423), powersets (mnupwd 41427), and an operation which is similar to a combination of collection and union (mnuop3d 41431), from which closure under pairing (mnuprd 41436), unions (mnuunid 41437), and function ranges (mnurnd 41443) can be deduced, from which equivalence with Grothendieck universes (grumnueq 41447) 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 488 . . . . . 6 ((𝑘 = 𝑈𝑙 = 𝑧) → 𝑙 = 𝑧)
21pweqd 4507 . . . . 5 ((𝑘 = 𝑈𝑙 = 𝑧) → 𝒫 𝑙 = 𝒫 𝑧)
3 simpl 486 . . . . 5 ((𝑘 = 𝑈𝑙 = 𝑧) → 𝑘 = 𝑈)
42, 3sseq12d 3910 . . . 4 ((𝑘 = 𝑈𝑙 = 𝑧) → (𝒫 𝑙𝑘 ↔ 𝒫 𝑧𝑈))
523adant3 1133 . . . . . . . . . 10 ((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) → 𝒫 𝑙 = 𝒫 𝑧)
65adantr 484 . . . . . . . . 9 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝒫 𝑙 = 𝒫 𝑧)
7 simpr 488 . . . . . . . . 9 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝑛 = 𝑤)
86, 7sseq12d 3910 . . . . . . . 8 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → (𝒫 𝑙𝑛 ↔ 𝒫 𝑧𝑤))
9 simpl3 1194 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑝 = 𝑖)
10 simpr 488 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑞 = 𝑣)
119, 10eleq12d 2827 . . . . . . . . . . . . 13 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → (𝑝𝑞𝑖𝑣))
12 simpl13 1251 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑚 = 𝑓)
1310, 12eleq12d 2827 . . . . . . . . . . . . 13 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → (𝑞𝑚𝑣𝑓))
1411, 13anbi12d 634 . . . . . . . . . . . 12 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → ((𝑝𝑞𝑞𝑚) ↔ (𝑖𝑣𝑣𝑓)))
15 simpl11 1249 . . . . . . . . . . . 12 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑘 = 𝑈)
1614, 15cbvrexdva2 3359 . . . . . . . . . . 11 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) → (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) ↔ ∃𝑣𝑈 (𝑖𝑣𝑣𝑓)))
17 simpl3 1194 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑝 = 𝑖)
18 simpr 488 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑟 = 𝑢)
1917, 18eleq12d 2827 . . . . . . . . . . . . 13 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → (𝑝𝑟𝑖𝑢))
2018unieqd 4810 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑟 = 𝑢)
21 simpl2 1193 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑛 = 𝑤)
2220, 21sseq12d 3910 . . . . . . . . . . . . 13 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → ( 𝑟𝑛 𝑢𝑤))
2319, 22anbi12d 634 . . . . . . . . . . . 12 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → ((𝑝𝑟 𝑟𝑛) ↔ (𝑖𝑢 𝑢𝑤)))
24 simpl13 1251 . . . . . . . . . . . 12 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑚 = 𝑓)
2523, 24cbvrexdva2 3359 . . . . . . . . . . 11 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) → (∃𝑟𝑚 (𝑝𝑟 𝑟𝑛) ↔ ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
2616, 25imbi12d 348 . . . . . . . . . 10 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) → ((∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)) ↔ (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
27263expa 1119 . . . . . . . . 9 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) ∧ 𝑝 = 𝑖) → ((∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)) ↔ (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
28 simpll2 1214 . . . . . . . . 9 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) ∧ 𝑝 = 𝑖) → 𝑙 = 𝑧)
2927, 28cbvraldva2 3358 . . . . . . . 8 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → (∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)) ↔ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
308, 29anbi12d 634 . . . . . . 7 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → ((𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))) ↔ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
31 simpl1 1192 . . . . . . 7 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝑘 = 𝑈)
3230, 31cbvrexdva2 3359 . . . . . 6 ((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) → (∃𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))) ↔ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
33323expa 1119 . . . . 5 (((𝑘 = 𝑈𝑙 = 𝑧) ∧ 𝑚 = 𝑓) → (∃𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))) ↔ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
3433cbvaldvaw 2050 . . . 4 ((𝑘 = 𝑈𝑙 = 𝑧) → (∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))) ↔ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
354, 34anbi12d 634 . . 3 ((𝑘 = 𝑈𝑙 = 𝑧) → ((𝒫 𝑙𝑘 ∧ ∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)))) ↔ (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))))
3635, 3cbvraldva2 3358 . 2 (𝑘 = 𝑈 → (∀𝑙𝑘 (𝒫 𝑙𝑘 ∧ ∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)))) ↔ ∀𝑧𝑈 (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))))
37 ismnu.1 . 2 𝑀 = {𝑘 ∣ ∀𝑙𝑘 (𝒫 𝑙𝑘 ∧ ∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))))}
3836, 37elab2g 3575 1 (𝑈𝑉 → (𝑈𝑀 ↔ ∀𝑧𝑈 (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1088  wal 1540   = wceq 1542  wcel 2114  {cab 2716  wral 3053  wrex 3054  wss 3843  𝒫 cpw 4488   cuni 4796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-rex 3059  df-v 3400  df-in 3850  df-ss 3860  df-pw 4490  df-uni 4797
This theorem is referenced by:  mnuop123d  41422  grumnudlem  41445  rr-grothprimbi  41455  rr-groth  41459
  Copyright terms: Public domain W3C validator