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

Theorem mnuop123d 42634
Description: Operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023.)
Hypotheses
Ref Expression
mnuop123d.1 𝑀 = {𝑘 ∣ ∀𝑙𝑘 (𝒫 𝑙𝑘 ∧ ∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))))}
mnuop123d.2 (𝜑𝑈𝑀)
mnuop123d.3 (𝜑𝐴𝑈)
Assertion
Ref Expression
mnuop123d (𝜑 → (𝒫 𝐴𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝐴𝑤 ∧ ∀𝑖𝐴 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
Distinct variable groups:   𝑤,𝐴,𝑓,𝑖   𝑤,𝑣,𝑈,𝑘,𝑚,𝑛,𝑞,𝑝,𝑙,𝑓,𝑖   𝑤,𝑢,𝑟,𝑈,𝑓,𝑖,𝑘,𝑚,𝑛,𝑝,𝑙
Allowed substitution hints:   𝜑(𝑤,𝑣,𝑢,𝑓,𝑖,𝑘,𝑚,𝑛,𝑟,𝑞,𝑝,𝑙)   𝐴(𝑣,𝑢,𝑘,𝑚,𝑛,𝑟,𝑞,𝑝,𝑙)   𝑀(𝑤,𝑣,𝑢,𝑓,𝑖,𝑘,𝑚,𝑛,𝑟,𝑞,𝑝,𝑙)

Proof of Theorem mnuop123d
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 pweq 4578 . . . 4 (𝑧 = 𝐴 → 𝒫 𝑧 = 𝒫 𝐴)
21sseq1d 3979 . . 3 (𝑧 = 𝐴 → (𝒫 𝑧𝑈 ↔ 𝒫 𝐴𝑈))
31sseq1d 3979 . . . . . 6 (𝑧 = 𝐴 → (𝒫 𝑧𝑤 ↔ 𝒫 𝐴𝑤))
4 raleq 3308 . . . . . 6 (𝑧 = 𝐴 → (∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ ∀𝑖𝐴 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
53, 4anbi12d 632 . . . . 5 (𝑧 = 𝐴 → ((𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ (𝒫 𝐴𝑤 ∧ ∀𝑖𝐴 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
65rexbidv 3172 . . . 4 (𝑧 = 𝐴 → (∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ ∃𝑤𝑈 (𝒫 𝐴𝑤 ∧ ∀𝑖𝐴 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
76albidv 1924 . . 3 (𝑧 = 𝐴 → (∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ ∀𝑓𝑤𝑈 (𝒫 𝐴𝑤 ∧ ∀𝑖𝐴 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
82, 7anbi12d 632 . 2 (𝑧 = 𝐴 → ((𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ (𝒫 𝐴𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝐴𝑤 ∧ ∀𝑖𝐴 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))))
9 mnuop123d.2 . . 3 (𝜑𝑈𝑀)
10 mnuop123d.1 . . . . 5 𝑀 = {𝑘 ∣ ∀𝑙𝑘 (𝒫 𝑙𝑘 ∧ ∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))))}
1110ismnu 42633 . . . 4 (𝑈𝑀 → (𝑈𝑀 ↔ ∀𝑧𝑈 (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))))
1211ibi 267 . . 3 (𝑈𝑀 → ∀𝑧𝑈 (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
139, 12syl 17 . 2 (𝜑 → ∀𝑧𝑈 (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
14 mnuop123d.3 . 2 (𝜑𝐴𝑈)
158, 13, 14rspcdva 3584 1 (𝜑 → (𝒫 𝐴𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝐴𝑤 ∧ ∀𝑖𝐴 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wal 1540   = wceq 1542  wcel 2107  {cab 2710  wral 3061  wrex 3070  wss 3914  𝒫 cpw 4564   cuni 4869
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rex 3071  df-v 3449  df-in 3921  df-ss 3931  df-pw 4566  df-uni 4870
This theorem is referenced by:  mnussd  42635  mnuop23d  42638
  Copyright terms: Public domain W3C validator