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

A minimal universe is closed under subsets (mnussd 43700), powersets (mnupwd 43704), and an operation which is similar to a combination of collection and union (mnuop3d 43708), from which closure under pairing (mnuprd 43713), unions (mnuunid 43714), and function ranges (mnurnd 43720) can be deduced, from which equivalence with Grothendieck universes (grumnueq 43724) 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 4620 . . . . 5 ((𝑘 = 𝑈𝑙 = 𝑧) → 𝒫 𝑙 = 𝒫 𝑧)
3 simpl 482 . . . . 5 ((𝑘 = 𝑈𝑙 = 𝑧) → 𝑘 = 𝑈)
42, 3sseq12d 4013 . . . 4 ((𝑘 = 𝑈𝑙 = 𝑧) → (𝒫 𝑙𝑘 ↔ 𝒫 𝑧𝑈))
523adant3 1130 . . . . . . . . . 10 ((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) → 𝒫 𝑙 = 𝒫 𝑧)
65adantr 480 . . . . . . . . 9 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝒫 𝑙 = 𝒫 𝑧)
7 simpr 484 . . . . . . . . 9 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝑛 = 𝑤)
86, 7sseq12d 4013 . . . . . . . 8 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → (𝒫 𝑙𝑛 ↔ 𝒫 𝑧𝑤))
9 simpl3 1191 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑝 = 𝑖)
10 simpr 484 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑞 = 𝑣)
119, 10eleq12d 2823 . . . . . . . . . . . . 13 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → (𝑝𝑞𝑖𝑣))
12 simpl13 1248 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑚 = 𝑓)
1310, 12eleq12d 2823 . . . . . . . . . . . . 13 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → (𝑞𝑚𝑣𝑓))
1411, 13anbi12d 631 . . . . . . . . . . . 12 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → ((𝑝𝑞𝑞𝑚) ↔ (𝑖𝑣𝑣𝑓)))
15 simpl11 1246 . . . . . . . . . . . 12 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑞 = 𝑣) → 𝑘 = 𝑈)
1614, 15cbvrexdva2 3342 . . . . . . . . . . 11 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) → (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) ↔ ∃𝑣𝑈 (𝑖𝑣𝑣𝑓)))
17 simpl3 1191 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑝 = 𝑖)
18 simpr 484 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑟 = 𝑢)
1917, 18eleq12d 2823 . . . . . . . . . . . . 13 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → (𝑝𝑟𝑖𝑢))
2018unieqd 4921 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑟 = 𝑢)
21 simpl2 1190 . . . . . . . . . . . . . 14 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑛 = 𝑤)
2220, 21sseq12d 4013 . . . . . . . . . . . . 13 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → ( 𝑟𝑛 𝑢𝑤))
2319, 22anbi12d 631 . . . . . . . . . . . 12 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → ((𝑝𝑟 𝑟𝑛) ↔ (𝑖𝑢 𝑢𝑤)))
24 simpl13 1248 . . . . . . . . . . . 12 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) ∧ 𝑟 = 𝑢) → 𝑚 = 𝑓)
2523, 24cbvrexdva2 3342 . . . . . . . . . . 11 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) → (∃𝑟𝑚 (𝑝𝑟 𝑟𝑛) ↔ ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
2616, 25imbi12d 344 . . . . . . . . . 10 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤𝑝 = 𝑖) → ((∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)) ↔ (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
27263expa 1116 . . . . . . . . 9 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) ∧ 𝑝 = 𝑖) → ((∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)) ↔ (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
28 simpll2 1211 . . . . . . . . 9 ((((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) ∧ 𝑝 = 𝑖) → 𝑙 = 𝑧)
2927, 28cbvraldva2 3341 . . . . . . . 8 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → (∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)) ↔ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
308, 29anbi12d 631 . . . . . . 7 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → ((𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))) ↔ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
31 simpl1 1189 . . . . . . 7 (((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) ∧ 𝑛 = 𝑤) → 𝑘 = 𝑈)
3230, 31cbvrexdva2 3342 . . . . . 6 ((𝑘 = 𝑈𝑙 = 𝑧𝑚 = 𝑓) → (∃𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))) ↔ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
33323expa 1116 . . . . 5 (((𝑘 = 𝑈𝑙 = 𝑧) ∧ 𝑚 = 𝑓) → (∃𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))) ↔ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
3433cbvaldvaw 2034 . . . 4 ((𝑘 = 𝑈𝑙 = 𝑧) → (∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))) ↔ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
354, 34anbi12d 631 . . 3 ((𝑘 = 𝑈𝑙 = 𝑧) → ((𝒫 𝑙𝑘 ∧ ∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)))) ↔ (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))))
3635, 3cbvraldva2 3341 . 2 (𝑘 = 𝑈 → (∀𝑙𝑘 (𝒫 𝑙𝑘 ∧ ∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛)))) ↔ ∀𝑧𝑈 (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))))
37 ismnu.1 . 2 𝑀 = {𝑘 ∣ ∀𝑙𝑘 (𝒫 𝑙𝑘 ∧ ∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))))}
3836, 37elab2g 3669 1 (𝑈𝑉 → (𝑈𝑀 ↔ ∀𝑧𝑈 (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1085  wal 1532   = wceq 1534  wcel 2099  {cab 2705  wral 3058  wrex 3067  wss 3947  𝒫 cpw 4603   cuni 4908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3059  df-rex 3068  df-v 3473  df-in 3954  df-ss 3964  df-pw 4605  df-uni 4909
This theorem is referenced by:  mnuop123d  43699  grumnudlem  43722  rr-grothprimbi  43732  rr-groth  43736  dfuniv2  43739
  Copyright terms: Public domain W3C validator