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 df-ss ⊢ ( 𝑣 ⊆ 𝑧 ↔ ∀ 𝑡 ( 𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧 ) )
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 ⊢ ( ∀ 𝑧 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑈 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑈 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤 ∈ 𝑈 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧 ) → ¬ ( 𝑣 ∈ 𝑈 → ¬ 𝑣 ∈ 𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖 ∈ 𝑧 → ( 𝑣 ∈ 𝑈 → ( 𝑖 ∈ 𝑣 → ( 𝑣 ∈ 𝑓 → ¬ ∀ 𝑢 ( 𝑢 ∈ 𝑓 → ( 𝑖 ∈ 𝑢 → ¬ ∀ 𝑜 ( 𝑜 ∈ 𝑢 → ∀ 𝑠 ( 𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤 ) ) ) ) ) ) ) ) ) ) ) )