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

Theorem ismnuprim 40127
 Description: Express the predicate on 𝑈 in ismnu 40094 using only primitives. (Contributed by Rohan Ridenour, 13-Aug-2023.)
Assertion
Ref Expression
ismnuprim (∀𝑧𝑈 (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ ∀𝑧(𝑧𝑈 → ∀𝑓 ¬ ∀𝑤(𝑤𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))))))))
Distinct variable groups:   𝑣,𝑢   𝑣,𝑖   𝑢,𝑜   𝑈,𝑓   𝑧,𝑤,𝑣   𝑧,𝑡,𝑣   𝑧,𝑓,𝑣   𝑤,𝑈,𝑣   𝑤,𝑜,𝑠
Allowed substitution hints:   𝑈(𝑧,𝑢,𝑡,𝑖,𝑜,𝑠)

Proof of Theorem ismnuprim
StepHypRef Expression
1 19.28v 1974 . . 3 (∀𝑓(𝒫 𝑧𝑈 ∧ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
2 r19.42v 3311 . . . . 5 (∃𝑤𝑈 (𝒫 𝑧𝑈 ∧ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ (𝒫 𝑧𝑈 ∧ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
3 19.26 1852 . . . . . . . 8 (∀𝑣((𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ (∀𝑣(𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑣𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
4 19.26 1852 . . . . . . . . . . 11 (∀𝑣((𝑣𝑧𝑣𝑈) ∧ (𝑣𝑧𝑣𝑤)) ↔ (∀𝑣(𝑣𝑧𝑣𝑈) ∧ ∀𝑣(𝑣𝑧𝑣𝑤)))
5 jcab 518 . . . . . . . . . . . 12 ((𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ↔ ((𝑣𝑧𝑣𝑈) ∧ (𝑣𝑧𝑣𝑤)))
65albii 1801 . . . . . . . . . . 11 (∀𝑣(𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ↔ ∀𝑣((𝑣𝑧𝑣𝑈) ∧ (𝑣𝑧𝑣𝑤)))
7 pwss 4470 . . . . . . . . . . . 12 (𝒫 𝑧𝑈 ↔ ∀𝑣(𝑣𝑧𝑣𝑈))
8 pwss 4470 . . . . . . . . . . . 12 (𝒫 𝑧𝑤 ↔ ∀𝑣(𝑣𝑧𝑣𝑤))
97, 8anbi12i 626 . . . . . . . . . . 11 ((𝒫 𝑧𝑈 ∧ 𝒫 𝑧𝑤) ↔ (∀𝑣(𝑣𝑧𝑣𝑈) ∧ ∀𝑣(𝑣𝑧𝑣𝑤)))
104, 6, 93bitr4i 304 . . . . . . . . . 10 (∀𝑣(𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ↔ (𝒫 𝑧𝑈 ∧ 𝒫 𝑧𝑤))
11 ralcom4 3199 . . . . . . . . . . 11 (∀𝑖𝑧𝑣((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ ∀𝑣𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
12 19.23v 1920 . . . . . . . . . . . . 13 (∀𝑣((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ (∃𝑣(𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
13 3anass 1088 . . . . . . . . . . . . . . . 16 ((𝑣𝑈𝑖𝑣𝑣𝑓) ↔ (𝑣𝑈 ∧ (𝑖𝑣𝑣𝑓)))
1413exbii 1829 . . . . . . . . . . . . . . 15 (∃𝑣(𝑣𝑈𝑖𝑣𝑣𝑓) ↔ ∃𝑣(𝑣𝑈 ∧ (𝑖𝑣𝑣𝑓)))
15 df-rex 3111 . . . . . . . . . . . . . . 15 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) ↔ ∃𝑣(𝑣𝑈 ∧ (𝑖𝑣𝑣𝑓)))
1614, 15bitr4i 279 . . . . . . . . . . . . . 14 (∃𝑣(𝑣𝑈𝑖𝑣𝑣𝑓) ↔ ∃𝑣𝑈 (𝑖𝑣𝑣𝑓))
1716imbi1i 351 . . . . . . . . . . . . 13 ((∃𝑣(𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
1812, 17bitri 276 . . . . . . . . . . . 12 (∀𝑣((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
1918ralbii 3132 . . . . . . . . . . 11 (∀𝑖𝑧𝑣((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
2011, 19bitr3i 278 . . . . . . . . . 10 (∀𝑣𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
2110, 20anbi12i 626 . . . . . . . . 9 ((∀𝑣(𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑣𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ ((𝒫 𝑧𝑈 ∧ 𝒫 𝑧𝑤) ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
22 anass 469 . . . . . . . . 9 (((𝒫 𝑧𝑈 ∧ 𝒫 𝑧𝑤) ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ (𝒫 𝑧𝑈 ∧ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
2321, 22bitri 276 . . . . . . . 8 ((∀𝑣(𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑣𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ (𝒫 𝑧𝑈 ∧ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
243, 23bitri 276 . . . . . . 7 (∀𝑣((𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ (𝒫 𝑧𝑈 ∧ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
25 dfss2 3877 . . . . . . . . . 10 (𝑣𝑧 ↔ ∀𝑡(𝑡𝑣𝑡𝑧))
26 df-an 397 . . . . . . . . . 10 ((𝑣𝑈𝑣𝑤) ↔ ¬ (𝑣𝑈 → ¬ 𝑣𝑤))
2725, 26imbi12i 352 . . . . . . . . 9 ((𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ↔ (∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)))
28 3impexp 1351 . . . . . . . . . . 11 (((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
29 biid 262 . . . . . . . . . . . . . . . 16 (𝑖𝑢𝑖𝑢)
30 expanduniss 40126 . . . . . . . . . . . . . . . 16 ( 𝑢𝑤 ↔ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))
3129, 30expandan 40121 . . . . . . . . . . . . . . 15 ((𝑖𝑢 𝑢𝑤) ↔ ¬ (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))
3231expandrexn 40124 . . . . . . . . . . . . . 14 (∃𝑢𝑓 (𝑖𝑢 𝑢𝑤) ↔ ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))
3332imbi2i 337 . . . . . . . . . . . . 13 ((𝑣𝑓 → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))
3433imbi2i 337 . . . . . . . . . . . 12 ((𝑖𝑣 → (𝑣𝑓 → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))))
3534imbi2i 337 . . . . . . . . . . 11 ((𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))))
3628, 35bitri 276 . . . . . . . . . 10 (((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))))
3736expandral 40123 . . . . . . . . 9 (∀𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))))))
3827, 37expandan 40121 . . . . . . . 8 (((𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))))))
3938albii 1801 . . . . . . 7 (∀𝑣((𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))))))
4024, 39bitr3i 278 . . . . . 6 ((𝒫 𝑧𝑈 ∧ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))))))
4140expandrex 40125 . . . . 5 (∃𝑤𝑈 (𝒫 𝑧𝑈 ∧ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ ¬ ∀𝑤(𝑤𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))))))))
422, 41bitr3i 278 . . . 4 ((𝒫 𝑧𝑈 ∧ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ ¬ ∀𝑤(𝑤𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))))))))
4342albii 1801 . . 3 (∀𝑓(𝒫 𝑧𝑈 ∧ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ ∀𝑓 ¬ ∀𝑤(𝑤𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))))))))
441, 43bitr3i 278 . 2 ((𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ ∀𝑓 ¬ ∀𝑤(𝑤𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))))))))
4544expandral 40123 1 (∀𝑧𝑈 (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ ∀𝑧(𝑧𝑈 → ∀𝑓 ¬ ∀𝑤(𝑤𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))))))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1080  ∀wal 1520  ∃wex 1761   ∈ wcel 2081  ∀wral 3105  ∃wrex 3106   ⊆ wss 3859  𝒫 cpw 4453  ∪ cuni 4745 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-v 3439  df-in 3866  df-ss 3874  df-pw 4455  df-uni 4746 This theorem is referenced by:  rr-grothprimbi  40128
 Copyright terms: Public domain W3C validator