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

Theorem ismnuprim 41173
 Description: Express the predicate on 𝑈 in ismnu 41140 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 1997 . . 3 (∀𝑓(𝒫 𝑧𝑈 ∧ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
2 r19.42v 3304 . . . . 5 (∃𝑤𝑈 (𝒫 𝑧𝑈 ∧ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ (𝒫 𝑧𝑈 ∧ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
3 19.26 1871 . . . . . . . 8 (∀𝑣((𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ (∀𝑣(𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑣𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
4 19.26 1871 . . . . . . . . . . 11 (∀𝑣((𝑣𝑧𝑣𝑈) ∧ (𝑣𝑧𝑣𝑤)) ↔ (∀𝑣(𝑣𝑧𝑣𝑈) ∧ ∀𝑣(𝑣𝑧𝑣𝑤)))
5 jcab 521 . . . . . . . . . . . 12 ((𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ↔ ((𝑣𝑧𝑣𝑈) ∧ (𝑣𝑧𝑣𝑤)))
65albii 1821 . . . . . . . . . . 11 (∀𝑣(𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ↔ ∀𝑣((𝑣𝑧𝑣𝑈) ∧ (𝑣𝑧𝑣𝑤)))
7 pwss 4525 . . . . . . . . . . . 12 (𝒫 𝑧𝑈 ↔ ∀𝑣(𝑣𝑧𝑣𝑈))
8 pwss 4525 . . . . . . . . . . . 12 (𝒫 𝑧𝑤 ↔ ∀𝑣(𝑣𝑧𝑣𝑤))
97, 8anbi12i 629 . . . . . . . . . . 11 ((𝒫 𝑧𝑈 ∧ 𝒫 𝑧𝑤) ↔ (∀𝑣(𝑣𝑧𝑣𝑈) ∧ ∀𝑣(𝑣𝑧𝑣𝑤)))
104, 6, 93bitr4i 306 . . . . . . . . . 10 (∀𝑣(𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ↔ (𝒫 𝑧𝑈 ∧ 𝒫 𝑧𝑤))
11 ralcom4 3198 . . . . . . . . . . 11 (∀𝑖𝑧𝑣((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ ∀𝑣𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
12 19.23v 1943 . . . . . . . . . . . . 13 (∀𝑣((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ (∃𝑣(𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
13 3anass 1092 . . . . . . . . . . . . . . . 16 ((𝑣𝑈𝑖𝑣𝑣𝑓) ↔ (𝑣𝑈 ∧ (𝑖𝑣𝑣𝑓)))
1413exbii 1849 . . . . . . . . . . . . . . 15 (∃𝑣(𝑣𝑈𝑖𝑣𝑣𝑓) ↔ ∃𝑣(𝑣𝑈 ∧ (𝑖𝑣𝑣𝑓)))
15 df-rex 3112 . . . . . . . . . . . . . . 15 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) ↔ ∃𝑣(𝑣𝑈 ∧ (𝑖𝑣𝑣𝑓)))
1614, 15bitr4i 281 . . . . . . . . . . . . . 14 (∃𝑣(𝑣𝑈𝑖𝑣𝑣𝑓) ↔ ∃𝑣𝑈 (𝑖𝑣𝑣𝑓))
1716imbi1i 353 . . . . . . . . . . . . 13 ((∃𝑣(𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
1812, 17bitri 278 . . . . . . . . . . . 12 (∀𝑣((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
1918ralbii 3133 . . . . . . . . . . 11 (∀𝑖𝑧𝑣((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
2011, 19bitr3i 280 . . . . . . . . . 10 (∀𝑣𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
2110, 20anbi12i 629 . . . . . . . . 9 ((∀𝑣(𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑣𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ ((𝒫 𝑧𝑈 ∧ 𝒫 𝑧𝑤) ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
22 anass 472 . . . . . . . . 9 (((𝒫 𝑧𝑈 ∧ 𝒫 𝑧𝑤) ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ (𝒫 𝑧𝑈 ∧ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
2321, 22bitri 278 . . . . . . . 8 ((∀𝑣(𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑣𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ (𝒫 𝑧𝑈 ∧ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
243, 23bitri 278 . . . . . . 7 (∀𝑣((𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ (𝒫 𝑧𝑈 ∧ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
25 dfss2 3903 . . . . . . . . . 10 (𝑣𝑧 ↔ ∀𝑡(𝑡𝑣𝑡𝑧))
26 df-an 400 . . . . . . . . . 10 ((𝑣𝑈𝑣𝑤) ↔ ¬ (𝑣𝑈 → ¬ 𝑣𝑤))
2725, 26imbi12i 354 . . . . . . . . 9 ((𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ↔ (∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)))
28 3impexp 1355 . . . . . . . . . . 11 (((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
29 biid 264 . . . . . . . . . . . . . . . 16 (𝑖𝑢𝑖𝑢)
30 expanduniss 41172 . . . . . . . . . . . . . . . 16 ( 𝑢𝑤 ↔ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))
3129, 30expandan 41167 . . . . . . . . . . . . . . 15 ((𝑖𝑢 𝑢𝑤) ↔ ¬ (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))
3231expandrexn 41170 . . . . . . . . . . . . . 14 (∃𝑢𝑓 (𝑖𝑢 𝑢𝑤) ↔ ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))
3332imbi2i 339 . . . . . . . . . . . . 13 ((𝑣𝑓 → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))
3433imbi2i 339 . . . . . . . . . . . 12 ((𝑖𝑣 → (𝑣𝑓 → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))))
3534imbi2i 339 . . . . . . . . . . 11 ((𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))))
3628, 35bitri 278 . . . . . . . . . 10 (((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))))
3736expandral 41169 . . . . . . . . 9 (∀𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))))))
3827, 37expandan 41167 . . . . . . . 8 (((𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))))))
3938albii 1821 . . . . . . 7 (∀𝑣((𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))))))
4024, 39bitr3i 280 . . . . . 6 ((𝒫 𝑧𝑈 ∧ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))))))
4140expandrex 41171 . . . . 5 (∃𝑤𝑈 (𝒫 𝑧𝑈 ∧ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ ¬ ∀𝑤(𝑤𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))))))))
422, 41bitr3i 280 . . . 4 ((𝒫 𝑧𝑈 ∧ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ ¬ ∀𝑤(𝑤𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))))))))
4342albii 1821 . . 3 (∀𝑓(𝒫 𝑧𝑈 ∧ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ ∀𝑓 ¬ ∀𝑤(𝑤𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))))))))
441, 43bitr3i 280 . 2 ((𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ ∀𝑓 ¬ ∀𝑤(𝑤𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))))))))
4544expandral 41169 1 (∀𝑧𝑈 (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ ∀𝑧(𝑧𝑈 → ∀𝑓 ¬ ∀𝑤(𝑤𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))))))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084  ∀wal 1536  ∃wex 1781   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107   ⊆ wss 3883  𝒫 cpw 4500  ∪ cuni 4804 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 2113  ax-9 2121  ax-11 2158  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3444  df-in 3890  df-ss 3900  df-pw 4502  df-uni 4805 This theorem is referenced by:  rr-grothprimbi  41174
 Copyright terms: Public domain W3C validator