Metamath Proof Explorer


Theorem ismnuprim

Description: Express the predicate on U in ismnu using only primitives. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Assertion ismnuprim ( ∀ 𝑧𝑈 ( 𝒫 𝑧𝑈 ∧ ∀ 𝑓𝑤𝑈 ( 𝒫 𝑧𝑤 ∧ ∀ 𝑖𝑧 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) ↔ ∀ 𝑧 ( 𝑧𝑈 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤𝑈 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡𝑣𝑡𝑧 ) → ¬ ( 𝑣𝑈 → ¬ 𝑣𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖𝑧 → ( 𝑣𝑈 → ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 19.28v ( ∀ 𝑓 ( 𝒫 𝑧𝑈 ∧ ∃ 𝑤𝑈 ( 𝒫 𝑧𝑤 ∧ ∀ 𝑖𝑧 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) ↔ ( 𝒫 𝑧𝑈 ∧ ∀ 𝑓𝑤𝑈 ( 𝒫 𝑧𝑤 ∧ ∀ 𝑖𝑧 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) )
2 r19.42v ( ∃ 𝑤𝑈 ( 𝒫 𝑧𝑈 ∧ ( 𝒫 𝑧𝑤 ∧ ∀ 𝑖𝑧 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) ↔ ( 𝒫 𝑧𝑈 ∧ ∃ 𝑤𝑈 ( 𝒫 𝑧𝑤 ∧ ∀ 𝑖𝑧 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) )
3 19.26 ( ∀ 𝑣 ( ( 𝑣𝑧 → ( 𝑣𝑈𝑣𝑤 ) ) ∧ ∀ 𝑖𝑧 ( ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ↔ ( ∀ 𝑣 ( 𝑣𝑧 → ( 𝑣𝑈𝑣𝑤 ) ) ∧ ∀ 𝑣𝑖𝑧 ( ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) )
4 19.26 ( ∀ 𝑣 ( ( 𝑣𝑧𝑣𝑈 ) ∧ ( 𝑣𝑧𝑣𝑤 ) ) ↔ ( ∀ 𝑣 ( 𝑣𝑧𝑣𝑈 ) ∧ ∀ 𝑣 ( 𝑣𝑧𝑣𝑤 ) ) )
5 jcab ( ( 𝑣𝑧 → ( 𝑣𝑈𝑣𝑤 ) ) ↔ ( ( 𝑣𝑧𝑣𝑈 ) ∧ ( 𝑣𝑧𝑣𝑤 ) ) )
6 5 albii ( ∀ 𝑣 ( 𝑣𝑧 → ( 𝑣𝑈𝑣𝑤 ) ) ↔ ∀ 𝑣 ( ( 𝑣𝑧𝑣𝑈 ) ∧ ( 𝑣𝑧𝑣𝑤 ) ) )
7 pwss ( 𝒫 𝑧𝑈 ↔ ∀ 𝑣 ( 𝑣𝑧𝑣𝑈 ) )
8 pwss ( 𝒫 𝑧𝑤 ↔ ∀ 𝑣 ( 𝑣𝑧𝑣𝑤 ) )
9 7 8 anbi12i ( ( 𝒫 𝑧𝑈 ∧ 𝒫 𝑧𝑤 ) ↔ ( ∀ 𝑣 ( 𝑣𝑧𝑣𝑈 ) ∧ ∀ 𝑣 ( 𝑣𝑧𝑣𝑤 ) ) )
10 4 6 9 3bitr4i ( ∀ 𝑣 ( 𝑣𝑧 → ( 𝑣𝑈𝑣𝑤 ) ) ↔ ( 𝒫 𝑧𝑈 ∧ 𝒫 𝑧𝑤 ) )
11 ralcom4 ( ∀ 𝑖𝑧𝑣 ( ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ↔ ∀ 𝑣𝑖𝑧 ( ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) )
12 19.23v ( ∀ 𝑣 ( ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ↔ ( ∃ 𝑣 ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) )
13 3anass ( ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) ↔ ( 𝑣𝑈 ∧ ( 𝑖𝑣𝑣𝑓 ) ) )
14 13 exbii ( ∃ 𝑣 ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) ↔ ∃ 𝑣 ( 𝑣𝑈 ∧ ( 𝑖𝑣𝑣𝑓 ) ) )
15 df-rex ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) ↔ ∃ 𝑣 ( 𝑣𝑈 ∧ ( 𝑖𝑣𝑣𝑓 ) ) )
16 14 15 bitr4i ( ∃ 𝑣 ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) ↔ ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) )
17 16 imbi1i ( ( ∃ 𝑣 ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ↔ ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) )
18 12 17 bitri ( ∀ 𝑣 ( ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ↔ ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) )
19 18 ralbii ( ∀ 𝑖𝑧𝑣 ( ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ↔ ∀ 𝑖𝑧 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) )
20 11 19 bitr3i ( ∀ 𝑣𝑖𝑧 ( ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ↔ ∀ 𝑖𝑧 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) )
21 10 20 anbi12i ( ( ∀ 𝑣 ( 𝑣𝑧 → ( 𝑣𝑈𝑣𝑤 ) ) ∧ ∀ 𝑣𝑖𝑧 ( ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ↔ ( ( 𝒫 𝑧𝑈 ∧ 𝒫 𝑧𝑤 ) ∧ ∀ 𝑖𝑧 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) )
22 anass ( ( ( 𝒫 𝑧𝑈 ∧ 𝒫 𝑧𝑤 ) ∧ ∀ 𝑖𝑧 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ↔ ( 𝒫 𝑧𝑈 ∧ ( 𝒫 𝑧𝑤 ∧ ∀ 𝑖𝑧 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) )
23 21 22 bitri ( ( ∀ 𝑣 ( 𝑣𝑧 → ( 𝑣𝑈𝑣𝑤 ) ) ∧ ∀ 𝑣𝑖𝑧 ( ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ↔ ( 𝒫 𝑧𝑈 ∧ ( 𝒫 𝑧𝑤 ∧ ∀ 𝑖𝑧 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) )
24 3 23 bitri ( ∀ 𝑣 ( ( 𝑣𝑧 → ( 𝑣𝑈𝑣𝑤 ) ) ∧ ∀ 𝑖𝑧 ( ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ↔ ( 𝒫 𝑧𝑈 ∧ ( 𝒫 𝑧𝑤 ∧ ∀ 𝑖𝑧 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) )
25 dfss2 ( 𝑣𝑧 ↔ ∀ 𝑡 ( 𝑡𝑣𝑡𝑧 ) )
26 df-an ( ( 𝑣𝑈𝑣𝑤 ) ↔ ¬ ( 𝑣𝑈 → ¬ 𝑣𝑤 ) )
27 25 26 imbi12i ( ( 𝑣𝑧 → ( 𝑣𝑈𝑣𝑤 ) ) ↔ ( ∀ 𝑡 ( 𝑡𝑣𝑡𝑧 ) → ¬ ( 𝑣𝑈 → ¬ 𝑣𝑤 ) ) )
28 3impexp ( ( ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ↔ ( 𝑣𝑈 → ( 𝑖𝑣 → ( 𝑣𝑓 → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) )
29 biid ( 𝑖𝑢𝑖𝑢 )
30 expanduniss ( 𝑢𝑤 ↔ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) )
31 29 30 expandan ( ( 𝑖𝑢 𝑢𝑤 ) ↔ ¬ ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) )
32 31 expandrexn ( ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ↔ ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) )
33 32 imbi2i ( ( 𝑣𝑓 → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ↔ ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) )
34 33 imbi2i ( ( 𝑖𝑣 → ( 𝑣𝑓 → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ↔ ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) )
35 34 imbi2i ( ( 𝑣𝑈 → ( 𝑖𝑣 → ( 𝑣𝑓 → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) ↔ ( 𝑣𝑈 → ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) ) )
36 28 35 bitri ( ( ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ↔ ( 𝑣𝑈 → ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) ) )
37 36 expandral ( ∀ 𝑖𝑧 ( ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ↔ ∀ 𝑖 ( 𝑖𝑧 → ( 𝑣𝑈 → ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) ) ) )
38 27 37 expandan ( ( ( 𝑣𝑧 → ( 𝑣𝑈𝑣𝑤 ) ) ∧ ∀ 𝑖𝑧 ( ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ↔ ¬ ( ( ∀ 𝑡 ( 𝑡𝑣𝑡𝑧 ) → ¬ ( 𝑣𝑈 → ¬ 𝑣𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖𝑧 → ( 𝑣𝑈 → ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) ) ) ) )
39 38 albii ( ∀ 𝑣 ( ( 𝑣𝑧 → ( 𝑣𝑈𝑣𝑤 ) ) ∧ ∀ 𝑖𝑧 ( ( 𝑣𝑈𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ↔ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡𝑣𝑡𝑧 ) → ¬ ( 𝑣𝑈 → ¬ 𝑣𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖𝑧 → ( 𝑣𝑈 → ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) ) ) ) )
40 24 39 bitr3i ( ( 𝒫 𝑧𝑈 ∧ ( 𝒫 𝑧𝑤 ∧ ∀ 𝑖𝑧 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) ↔ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡𝑣𝑡𝑧 ) → ¬ ( 𝑣𝑈 → ¬ 𝑣𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖𝑧 → ( 𝑣𝑈 → ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) ) ) ) )
41 40 expandrex ( ∃ 𝑤𝑈 ( 𝒫 𝑧𝑈 ∧ ( 𝒫 𝑧𝑤 ∧ ∀ 𝑖𝑧 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) ↔ ¬ ∀ 𝑤 ( 𝑤𝑈 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡𝑣𝑡𝑧 ) → ¬ ( 𝑣𝑈 → ¬ 𝑣𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖𝑧 → ( 𝑣𝑈 → ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) ) ) ) ) )
42 2 41 bitr3i ( ( 𝒫 𝑧𝑈 ∧ ∃ 𝑤𝑈 ( 𝒫 𝑧𝑤 ∧ ∀ 𝑖𝑧 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) ↔ ¬ ∀ 𝑤 ( 𝑤𝑈 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡𝑣𝑡𝑧 ) → ¬ ( 𝑣𝑈 → ¬ 𝑣𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖𝑧 → ( 𝑣𝑈 → ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) ) ) ) ) )
43 42 albii ( ∀ 𝑓 ( 𝒫 𝑧𝑈 ∧ ∃ 𝑤𝑈 ( 𝒫 𝑧𝑤 ∧ ∀ 𝑖𝑧 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) ↔ ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤𝑈 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡𝑣𝑡𝑧 ) → ¬ ( 𝑣𝑈 → ¬ 𝑣𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖𝑧 → ( 𝑣𝑈 → ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) ) ) ) ) )
44 1 43 bitr3i ( ( 𝒫 𝑧𝑈 ∧ ∀ 𝑓𝑤𝑈 ( 𝒫 𝑧𝑤 ∧ ∀ 𝑖𝑧 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) ↔ ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤𝑈 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡𝑣𝑡𝑧 ) → ¬ ( 𝑣𝑈 → ¬ 𝑣𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖𝑧 → ( 𝑣𝑈 → ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) ) ) ) ) )
45 44 expandral ( ∀ 𝑧𝑈 ( 𝒫 𝑧𝑈 ∧ ∀ 𝑓𝑤𝑈 ( 𝒫 𝑧𝑤 ∧ ∀ 𝑖𝑧 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) ↔ ∀ 𝑧 ( 𝑧𝑈 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤𝑈 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡𝑣𝑡𝑧 ) → ¬ ( 𝑣𝑈 → ¬ 𝑣𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖𝑧 → ( 𝑣𝑈 → ( 𝑖𝑣 → ( 𝑣𝑓 → ¬ ∀ 𝑢 ( 𝑢𝑓 → ( 𝑖𝑢 → ¬ ∀ 𝑜 ( 𝑜𝑢 → ∀ 𝑠 ( 𝑠𝑜𝑠𝑤 ) ) ) ) ) ) ) ) ) ) ) )