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

Theorem mnuprdlem4 40917
Description: Lemma for mnuprd 40918. General case. (Contributed by Rohan Ridenour, 13-Aug-2023.)
Hypotheses
Ref Expression
mnuprdlem4.1 𝑀 = {𝑘 ∣ ∀𝑙𝑘 (𝒫 𝑙𝑘 ∧ ∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))))}
mnuprdlem4.2 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}
mnuprdlem4.3 (𝜑𝑈𝑀)
mnuprdlem4.4 (𝜑𝐴𝑈)
mnuprdlem4.5 (𝜑𝐵𝑈)
mnuprdlem4.6 (𝜑 → ¬ 𝐴 = ∅)
Assertion
Ref Expression
mnuprdlem4 (𝜑 → {𝐴, 𝐵} ∈ 𝑈)
Distinct variable groups:   𝑈,𝑘,𝑚,𝑛,𝑞,𝑝,𝑙   𝑈,𝑟,𝑘,𝑚,𝑛,𝑝,𝑙
Allowed substitution hints:   𝜑(𝑘,𝑚,𝑛,𝑟,𝑞,𝑝,𝑙)   𝐴(𝑘,𝑚,𝑛,𝑟,𝑞,𝑝,𝑙)   𝐵(𝑘,𝑚,𝑛,𝑟,𝑞,𝑝,𝑙)   𝐹(𝑘,𝑚,𝑛,𝑟,𝑞,𝑝,𝑙)   𝑀(𝑘,𝑚,𝑛,𝑟,𝑞,𝑝,𝑙)

Proof of Theorem mnuprdlem4
Dummy variables 𝑣 𝑤 𝑎 𝑖 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mnuprdlem4.1 . . . 4 𝑀 = {𝑘 ∣ ∀𝑙𝑘 (𝒫 𝑙𝑘 ∧ ∀𝑚𝑛𝑘 (𝒫 𝑙𝑛 ∧ ∀𝑝𝑙 (∃𝑞𝑘 (𝑝𝑞𝑞𝑚) → ∃𝑟𝑚 (𝑝𝑟 𝑟𝑛))))}
2 mnuprdlem4.3 . . . 4 (𝜑𝑈𝑀)
3 mnuprdlem4.4 . . . . . . 7 (𝜑𝐴𝑈)
41, 2, 3mnu0eld 40907 . . . . . 6 (𝜑 → ∅ ∈ 𝑈)
51, 2, 4mnusnd 40910 . . . . 5 (𝜑 → {∅} ∈ 𝑈)
6 0ss 4322 . . . . 5 ∅ ⊆ {∅}
7 ssid 3964 . . . . 5 {∅} ⊆ {∅}
81, 2, 5, 6, 7mnuprss2d 40912 . . . 4 (𝜑 → {∅, {∅}} ∈ 𝑈)
9 mnuprdlem4.2 . . . . 5 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}
101, 2, 3mnusnd 40910 . . . . . . 7 (𝜑 → {𝐴} ∈ 𝑈)
11 0ss 4322 . . . . . . 7 ∅ ⊆ {𝐴}
12 ssid 3964 . . . . . . 7 {𝐴} ⊆ {𝐴}
131, 2, 10, 11, 12mnuprss2d 40912 . . . . . 6 (𝜑 → {∅, {𝐴}} ∈ 𝑈)
14 mnuprdlem4.5 . . . . . . . 8 (𝜑𝐵𝑈)
15 0ss 4322 . . . . . . . 8 ∅ ⊆ 𝐵
16 ssid 3964 . . . . . . . 8 𝐵𝐵
171, 2, 14, 15, 16mnuprss2d 40912 . . . . . . 7 (𝜑 → {∅, 𝐵} ∈ 𝑈)
18 snsspr1 4720 . . . . . . 7 {∅} ⊆ {∅, 𝐵}
19 snsspr2 4721 . . . . . . 7 {𝐵} ⊆ {∅, 𝐵}
201, 2, 17, 18, 19mnuprss2d 40912 . . . . . 6 (𝜑 → {{∅}, {𝐵}} ∈ 𝑈)
2113, 20prssd 4728 . . . . 5 (𝜑 → {{∅, {𝐴}}, {{∅}, {𝐵}}} ⊆ 𝑈)
229, 21eqsstrid 3990 . . . 4 (𝜑𝐹𝑈)
231, 2, 8, 22mnuop3d 40913 . . 3 (𝜑 → ∃𝑤𝑈𝑖 ∈ {∅, {∅}} (∃𝑣𝐹 𝑖𝑣 → ∃𝑢𝐹 (𝑖𝑢 𝑢𝑤)))
24 simprl 770 . . . 4 ((𝜑 ∧ (𝑤𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣𝐹 𝑖𝑣 → ∃𝑢𝐹 (𝑖𝑢 𝑢𝑤)))) → 𝑤𝑈)
25 eleq2w 2897 . . . . . 6 (𝑎 = 𝑤 → (𝐴𝑎𝐴𝑤))
26 eleq2w 2897 . . . . . 6 (𝑎 = 𝑤 → (𝐵𝑎𝐵𝑤))
2725, 26anbi12d 633 . . . . 5 (𝑎 = 𝑤 → ((𝐴𝑎𝐵𝑎) ↔ (𝐴𝑤𝐵𝑤)))
2827adantl 485 . . . 4 (((𝜑 ∧ (𝑤𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣𝐹 𝑖𝑣 → ∃𝑢𝐹 (𝑖𝑢 𝑢𝑤)))) ∧ 𝑎 = 𝑤) → ((𝐴𝑎𝐵𝑎) ↔ (𝐴𝑤𝐵𝑤)))
293adantr 484 . . . . . 6 ((𝜑 ∧ (𝑤𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣𝐹 𝑖𝑣 → ∃𝑢𝐹 (𝑖𝑢 𝑢𝑤)))) → 𝐴𝑈)
3014adantr 484 . . . . . 6 ((𝜑 ∧ (𝑤𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣𝐹 𝑖𝑣 → ∃𝑢𝐹 (𝑖𝑢 𝑢𝑤)))) → 𝐵𝑈)
31 nfv 1915 . . . . . . . . 9 𝑖𝜑
32 nfv 1915 . . . . . . . . . 10 𝑖 𝑤𝑈
33 nfra1 3208 . . . . . . . . . 10 𝑖𝑖 ∈ {∅, {∅}} (∃𝑣𝐹 𝑖𝑣 → ∃𝑢𝐹 (𝑖𝑢 𝑢𝑤))
3432, 33nfan 1900 . . . . . . . . 9 𝑖(𝑤𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣𝐹 𝑖𝑣 → ∃𝑢𝐹 (𝑖𝑢 𝑢𝑤)))
3531, 34nfan 1900 . . . . . . . 8 𝑖(𝜑 ∧ (𝑤𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣𝐹 𝑖𝑣 → ∃𝑢𝐹 (𝑖𝑢 𝑢𝑤))))
369, 35mnuprdlem3 40916 . . . . . . 7 ((𝜑 ∧ (𝑤𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣𝐹 𝑖𝑣 → ∃𝑢𝐹 (𝑖𝑢 𝑢𝑤)))) → ∀𝑖 ∈ {∅, {∅}}∃𝑣𝐹 𝑖𝑣)
37 ralim 3154 . . . . . . . 8 (∀𝑖 ∈ {∅, {∅}} (∃𝑣𝐹 𝑖𝑣 → ∃𝑢𝐹 (𝑖𝑢 𝑢𝑤)) → (∀𝑖 ∈ {∅, {∅}}∃𝑣𝐹 𝑖𝑣 → ∀𝑖 ∈ {∅, {∅}}∃𝑢𝐹 (𝑖𝑢 𝑢𝑤)))
3837ad2antll 728 . . . . . . 7 ((𝜑 ∧ (𝑤𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣𝐹 𝑖𝑣 → ∃𝑢𝐹 (𝑖𝑢 𝑢𝑤)))) → (∀𝑖 ∈ {∅, {∅}}∃𝑣𝐹 𝑖𝑣 → ∀𝑖 ∈ {∅, {∅}}∃𝑢𝐹 (𝑖𝑢 𝑢𝑤)))
3936, 38mpd 15 . . . . . 6 ((𝜑 ∧ (𝑤𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣𝐹 𝑖𝑣 → ∃𝑢𝐹 (𝑖𝑢 𝑢𝑤)))) → ∀𝑖 ∈ {∅, {∅}}∃𝑢𝐹 (𝑖𝑢 𝑢𝑤))
409, 29, 30, 39mnuprdlem1 40914 . . . . 5 ((𝜑 ∧ (𝑤𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣𝐹 𝑖𝑣 → ∃𝑢𝐹 (𝑖𝑢 𝑢𝑤)))) → 𝐴𝑤)
41 mnuprdlem4.6 . . . . . . 7 (𝜑 → ¬ 𝐴 = ∅)
4241adantr 484 . . . . . 6 ((𝜑 ∧ (𝑤𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣𝐹 𝑖𝑣 → ∃𝑢𝐹 (𝑖𝑢 𝑢𝑤)))) → ¬ 𝐴 = ∅)
439, 30, 42, 39mnuprdlem2 40915 . . . . 5 ((𝜑 ∧ (𝑤𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣𝐹 𝑖𝑣 → ∃𝑢𝐹 (𝑖𝑢 𝑢𝑤)))) → 𝐵𝑤)
4440, 43jca 515 . . . 4 ((𝜑 ∧ (𝑤𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣𝐹 𝑖𝑣 → ∃𝑢𝐹 (𝑖𝑢 𝑢𝑤)))) → (𝐴𝑤𝐵𝑤))
4524, 28, 44rspcedvd 3601 . . 3 ((𝜑 ∧ (𝑤𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣𝐹 𝑖𝑣 → ∃𝑢𝐹 (𝑖𝑢 𝑢𝑤)))) → ∃𝑎𝑈 (𝐴𝑎𝐵𝑎))
4623, 45rexlimddv 3277 . 2 (𝜑 → ∃𝑎𝑈 (𝐴𝑎𝐵𝑎))
472adantr 484 . . 3 ((𝜑 ∧ (𝑎𝑈 ∧ (𝐴𝑎𝐵𝑎))) → 𝑈𝑀)
48 simprl 770 . . 3 ((𝜑 ∧ (𝑎𝑈 ∧ (𝐴𝑎𝐵𝑎))) → 𝑎𝑈)
49 simprrl 780 . . . 4 ((𝜑 ∧ (𝑎𝑈 ∧ (𝐴𝑎𝐵𝑎))) → 𝐴𝑎)
50 simprrr 781 . . . 4 ((𝜑 ∧ (𝑎𝑈 ∧ (𝐴𝑎𝐵𝑎))) → 𝐵𝑎)
5149, 50prssd 4728 . . 3 ((𝜑 ∧ (𝑎𝑈 ∧ (𝐴𝑎𝐵𝑎))) → {𝐴, 𝐵} ⊆ 𝑎)
521, 47, 48, 51mnussd 40905 . 2 ((𝜑 ∧ (𝑎𝑈 ∧ (𝐴𝑎𝐵𝑎))) → {𝐴, 𝐵} ∈ 𝑈)
5346, 52rexlimddv 3277 1 (𝜑 → {𝐴, 𝐵} ∈ 𝑈)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wal 1536   = wceq 1538  wcel 2114  {cab 2800  wral 3130  wrex 3131  wss 3908  c0 4265  𝒫 cpw 4511  {csn 4539  {cpr 4541   cuni 4813
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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-ral 3135  df-rex 3136  df-rab 3139  df-v 3471  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-pw 4513  df-sn 4540  df-pr 4542  df-uni 4814
This theorem is referenced by:  mnuprd  40918
  Copyright terms: Public domain W3C validator