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

Theorem ismnuprim 41585
Description: Express the predicate on 𝑈 in ismnu 41552 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 1999 . . 3 (∀𝑓(𝒫 𝑧𝑈 ∧ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
2 r19.42v 3263 . . . . 5 (∃𝑤𝑈 (𝒫 𝑧𝑈 ∧ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ (𝒫 𝑧𝑈 ∧ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
3 19.26 1878 . . . . . . . 8 (∀𝑣((𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ (∀𝑣(𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑣𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
4 19.26 1878 . . . . . . . . . . 11 (∀𝑣((𝑣𝑧𝑣𝑈) ∧ (𝑣𝑧𝑣𝑤)) ↔ (∀𝑣(𝑣𝑧𝑣𝑈) ∧ ∀𝑣(𝑣𝑧𝑣𝑤)))
5 jcab 521 . . . . . . . . . . . 12 ((𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ↔ ((𝑣𝑧𝑣𝑈) ∧ (𝑣𝑧𝑣𝑤)))
65albii 1827 . . . . . . . . . . 11 (∀𝑣(𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ↔ ∀𝑣((𝑣𝑧𝑣𝑈) ∧ (𝑣𝑧𝑣𝑤)))
7 pwss 4538 . . . . . . . . . . . 12 (𝒫 𝑧𝑈 ↔ ∀𝑣(𝑣𝑧𝑣𝑈))
8 pwss 4538 . . . . . . . . . . . 12 (𝒫 𝑧𝑤 ↔ ∀𝑣(𝑣𝑧𝑣𝑤))
97, 8anbi12i 630 . . . . . . . . . . 11 ((𝒫 𝑧𝑈 ∧ 𝒫 𝑧𝑤) ↔ (∀𝑣(𝑣𝑧𝑣𝑈) ∧ ∀𝑣(𝑣𝑧𝑣𝑤)))
104, 6, 93bitr4i 306 . . . . . . . . . 10 (∀𝑣(𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ↔ (𝒫 𝑧𝑈 ∧ 𝒫 𝑧𝑤))
11 ralcom4 3157 . . . . . . . . . . 11 (∀𝑖𝑧𝑣((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ ∀𝑣𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
12 19.23v 1950 . . . . . . . . . . . . 13 (∀𝑣((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ (∃𝑣(𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
13 3anass 1097 . . . . . . . . . . . . . . . 16 ((𝑣𝑈𝑖𝑣𝑣𝑓) ↔ (𝑣𝑈 ∧ (𝑖𝑣𝑣𝑓)))
1413exbii 1855 . . . . . . . . . . . . . . 15 (∃𝑣(𝑣𝑈𝑖𝑣𝑣𝑓) ↔ ∃𝑣(𝑣𝑈 ∧ (𝑖𝑣𝑣𝑓)))
15 df-rex 3067 . . . . . . . . . . . . . . 15 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) ↔ ∃𝑣(𝑣𝑈 ∧ (𝑖𝑣𝑣𝑓)))
1614, 15bitr4i 281 . . . . . . . . . . . . . 14 (∃𝑣(𝑣𝑈𝑖𝑣𝑣𝑓) ↔ ∃𝑣𝑈 (𝑖𝑣𝑣𝑓))
1716imbi1i 353 . . . . . . . . . . . . 13 ((∃𝑣(𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
1812, 17bitri 278 . . . . . . . . . . . 12 (∀𝑣((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
1918ralbii 3088 . . . . . . . . . . 11 (∀𝑖𝑧𝑣((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
2011, 19bitr3i 280 . . . . . . . . . 10 (∀𝑣𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))
2110, 20anbi12i 630 . . . . . . . . 9 ((∀𝑣(𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑣𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ ((𝒫 𝑧𝑈 ∧ 𝒫 𝑧𝑤) ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))))
22 anass 472 . . . . . . . . 9 (((𝒫 𝑧𝑈 ∧ 𝒫 𝑧𝑤) ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ (𝒫 𝑧𝑈 ∧ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
2321, 22bitri 278 . . . . . . . 8 ((∀𝑣(𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑣𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ (𝒫 𝑧𝑈 ∧ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
243, 23bitri 278 . . . . . . 7 (∀𝑣((𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ (𝒫 𝑧𝑈 ∧ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
25 dfss2 3886 . . . . . . . . . 10 (𝑣𝑧 ↔ ∀𝑡(𝑡𝑣𝑡𝑧))
26 df-an 400 . . . . . . . . . 10 ((𝑣𝑈𝑣𝑤) ↔ ¬ (𝑣𝑈 → ¬ 𝑣𝑤))
2725, 26imbi12i 354 . . . . . . . . 9 ((𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ↔ (∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)))
28 3impexp 1360 . . . . . . . . . . 11 (((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))))
29 biid 264 . . . . . . . . . . . . . . . 16 (𝑖𝑢𝑖𝑢)
30 expanduniss 41584 . . . . . . . . . . . . . . . 16 ( 𝑢𝑤 ↔ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))
3129, 30expandan 41579 . . . . . . . . . . . . . . 15 ((𝑖𝑢 𝑢𝑤) ↔ ¬ (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))
3231expandrexn 41582 . . . . . . . . . . . . . 14 (∃𝑢𝑓 (𝑖𝑢 𝑢𝑤) ↔ ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))
3332imbi2i 339 . . . . . . . . . . . . 13 ((𝑣𝑓 → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))
3433imbi2i 339 . . . . . . . . . . . 12 ((𝑖𝑣 → (𝑣𝑓 → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))))
3534imbi2i 339 . . . . . . . . . . 11 ((𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))))
3628, 35bitri 278 . . . . . . . . . 10 (((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))))
3736expandral 41581 . . . . . . . . 9 (∀𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)) ↔ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))))))
3827, 37expandan 41579 . . . . . . . 8 (((𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))))))
3938albii 1827 . . . . . . 7 (∀𝑣((𝑣𝑧 → (𝑣𝑈𝑣𝑤)) ∧ ∀𝑖𝑧 ((𝑣𝑈𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤))) ↔ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))))))
4024, 39bitr3i 280 . . . . . 6 ((𝒫 𝑧𝑈 ∧ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))))))
4140expandrex 41583 . . . . 5 (∃𝑤𝑈 (𝒫 𝑧𝑈 ∧ (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ ¬ ∀𝑤(𝑤𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))))))))
422, 41bitr3i 280 . . . 4 ((𝒫 𝑧𝑈 ∧ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ ¬ ∀𝑤(𝑤𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))))))))
4342albii 1827 . . 3 (∀𝑓(𝒫 𝑧𝑈 ∧ ∃𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ ∀𝑓 ¬ ∀𝑤(𝑤𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))))))))
441, 43bitr3i 280 . 2 ((𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ ∀𝑓 ¬ ∀𝑤(𝑤𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤)))))))))))
4544expandral 41581 1 (∀𝑧𝑈 (𝒫 𝑧𝑈 ∧ ∀𝑓𝑤𝑈 (𝒫 𝑧𝑤 ∧ ∀𝑖𝑧 (∃𝑣𝑈 (𝑖𝑣𝑣𝑓) → ∃𝑢𝑓 (𝑖𝑢 𝑢𝑤)))) ↔ ∀𝑧(𝑧𝑈 → ∀𝑓 ¬ ∀𝑤(𝑤𝑈 → ¬ ∀𝑣 ¬ ((∀𝑡(𝑡𝑣𝑡𝑧) → ¬ (𝑣𝑈 → ¬ 𝑣𝑤)) → ¬ ∀𝑖(𝑖𝑧 → (𝑣𝑈 → (𝑖𝑣 → (𝑣𝑓 → ¬ ∀𝑢(𝑢𝑓 → (𝑖𝑢 → ¬ ∀𝑜(𝑜𝑢 → ∀𝑠(𝑠𝑜𝑠𝑤))))))))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1089  wal 1541  wex 1787  wcel 2110  wral 3061  wrex 3062  wss 3866  𝒫 cpw 4513   cuni 4819
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-11 2158  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-v 3410  df-in 3873  df-ss 3883  df-pw 4515  df-uni 4820
This theorem is referenced by:  rr-grothprimbi  41586
  Copyright terms: Public domain W3C validator