Metamath Proof Explorer

Theorem ismnushort

Description: Express the predicate on U and z in ismnu in a shorter form while avoiding complicated definitions. (Contributed by Rohan Ridenour, 10-Oct-2024)

Ref Expression
Assertion ismnushort ( ∀ 𝑓 ∈ 𝒫 𝑈 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ↔ ( 𝒫 𝑧 ⊆ 𝑈 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) → 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) )
2 1 reximi ⊢ ( ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) → ∃ 𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) )
3 2 ralimi ⊢ ( ∀ 𝑓 ∈ 𝒫 𝑈 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) → ∀ 𝑓 ∈ 𝒫 𝑈 ∃ 𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) )
4 0elpw ⊢ ∅ ∈ 𝒫 𝑈
5 4 a1i ⊢ ( ⊤ → ∅ ∈ 𝒫 𝑈 )
6 biidd ⊢ ( ( ⊤ ∧ 𝑓 = ∅ ) → ( ∃ 𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ↔ ∃ 𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ) )
7 5 6 rspcdv ⊢ ( ⊤ → ( ∀ 𝑓 ∈ 𝒫 𝑈 ∃ 𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) → ∃ 𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ) )
8 7 mptru ⊢ ( ∀ 𝑓 ∈ 𝒫 𝑈 ∃ 𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) → ∃ 𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) )
9 inss1 ⊢ ( 𝑈 ∩ 𝑤 ) ⊆ 𝑈
10 sstr2 ⊢ ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) → ( ( 𝑈 ∩ 𝑤 ) ⊆ 𝑈 → 𝒫 𝑧 ⊆ 𝑈 ) )
11 9 10 mpi ⊢ ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) → 𝒫 𝑧 ⊆ 𝑈 )
12 11 reximi ⊢ ( ∃ 𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) → ∃ 𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ 𝑈 )
13 8 12 syl ⊢ ( ∀ 𝑓 ∈ 𝒫 𝑈 ∃ 𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) → ∃ 𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ 𝑈 )
14 rexex ⊢ ( ∃ 𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ 𝑈 → ∃ 𝑤 𝒫 𝑧 ⊆ 𝑈 )
15 ax5e ⊢ ( ∃ 𝑤 𝒫 𝑧 ⊆ 𝑈 → 𝒫 𝑧 ⊆ 𝑈 )
16 14 15 syl ⊢ ( ∃ 𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ 𝑈 → 𝒫 𝑧 ⊆ 𝑈 )
17 3 13 16 3syl ⊢ ( ∀ 𝑓 ∈ 𝒫 𝑈 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) → 𝒫 𝑧 ⊆ 𝑈 )
18 inss1 ⊢ ( 𝑈 ∩ 𝑔 ) ⊆ 𝑈
19 vex ⊢ 𝑔 ∈ V
20 19 inex2 ⊢ ( 𝑈 ∩ 𝑔 ) ∈ V
21 20 elpw ⊢ ( ( 𝑈 ∩ 𝑔 ) ∈ 𝒫 𝑈 ↔ ( 𝑈 ∩ 𝑔 ) ⊆ 𝑈 )
22 18 21 mpbir ⊢ ( 𝑈 ∩ 𝑔 ) ∈ 𝒫 𝑈
23 unieq ⊢ ( 𝑓 = ( 𝑈 ∩ 𝑔 ) → ∪ 𝑓 = ∪ ( 𝑈 ∩ 𝑔 ) )
24 23 ineq2d ⊢ ( 𝑓 = ( 𝑈 ∩ 𝑔 ) → ( 𝑧 ∩ ∪ 𝑓 ) = ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) )
25 ineq1 ⊢ ( 𝑓 = ( 𝑈 ∩ 𝑔 ) → ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) = ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) )
26 25 unieqd ⊢ ( 𝑓 = ( 𝑈 ∩ 𝑔 ) → ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) = ∪ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) )
27 24 26 sseq12d ⊢ ( 𝑓 = ( 𝑈 ∩ 𝑔 ) → ( ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ↔ ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) ⊆ ∪ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ) )
28 27 anbi2d ⊢ ( 𝑓 = ( 𝑈 ∩ 𝑔 ) → ( ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ↔ ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) ⊆ ∪ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ) ) )
29 28 rexbidv ⊢ ( 𝑓 = ( 𝑈 ∩ 𝑔 ) → ( ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ↔ ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) ⊆ ∪ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ) ) )
30 29 rspcv ⊢ ( ( 𝑈 ∩ 𝑔 ) ∈ 𝒫 𝑈 → ( ∀ 𝑓 ∈ 𝒫 𝑈 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) ⊆ ∪ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ) ) )
31 22 30 ax-mp ⊢ ( ∀ 𝑓 ∈ 𝒫 𝑈 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) ⊆ ∪ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ) )
32 31 alrimiv ⊢ ( ∀ 𝑓 ∈ 𝒫 𝑈 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) → ∀ 𝑔 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) ⊆ ∪ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ) )
33 inss2 ⊢ ( 𝑈 ∩ 𝑤 ) ⊆ 𝑤
34 sstr2 ⊢ ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) → ( ( 𝑈 ∩ 𝑤 ) ⊆ 𝑤 → 𝒫 𝑧 ⊆ 𝑤 ) )
35 33 34 mpi ⊢ ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) → 𝒫 𝑧 ⊆ 𝑤 )
36 an12 ⊢ ( ( 𝑣 ∈ 𝑈 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔 ) ) ↔ ( 𝑖 ∈ 𝑣 ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔 ) ) )
37 elin ⊢ ( 𝑣 ∈ ( 𝑈 ∩ 𝑔 ) ↔ ( 𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔 ) )
38 37 bicomi ⊢ ( ( 𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔 ) ↔ 𝑣 ∈ ( 𝑈 ∩ 𝑔 ) )
39 38 anbi2i ⊢ ( ( 𝑖 ∈ 𝑣 ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔 ) ) ↔ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ ( 𝑈 ∩ 𝑔 ) ) )
40 36 39 bitri ⊢ ( ( 𝑣 ∈ 𝑈 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔 ) ) ↔ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ ( 𝑈 ∩ 𝑔 ) ) )
41 40 exbii ⊢ ( ∃ 𝑣 ( 𝑣 ∈ 𝑈 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔 ) ) ↔ ∃ 𝑣 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ ( 𝑈 ∩ 𝑔 ) ) )
42 df-rex ⊢ ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔 ) ↔ ∃ 𝑣 ( 𝑣 ∈ 𝑈 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔 ) ) )
43 eluni ⊢ ( 𝑖 ∈ ∪ ( 𝑈 ∩ 𝑔 ) ↔ ∃ 𝑣 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ ( 𝑈 ∩ 𝑔 ) ) )
44 41 42 43 3bitr4i ⊢ ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔 ) ↔ 𝑖 ∈ ∪ ( 𝑈 ∩ 𝑔 ) )
45 simp1 ⊢ ( ( ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) ⊆ ∪ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ ( 𝑈 ∩ 𝑔 ) ) → ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) ⊆ ∪ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) )
46 elin ⊢ ( 𝑖 ∈ ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) ↔ ( 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ ( 𝑈 ∩ 𝑔 ) ) )
47 46 biimpri ⊢ ( ( 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ ( 𝑈 ∩ 𝑔 ) ) → 𝑖 ∈ ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) )
48 47 3adant1 ⊢ ( ( ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) ⊆ ∪ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ ( 𝑈 ∩ 𝑔 ) ) → 𝑖 ∈ ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) )
49 45 48 sseldd ⊢ ( ( ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) ⊆ ∪ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ ( 𝑈 ∩ 𝑔 ) ) → 𝑖 ∈ ∪ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) )
50 eluni ⊢ ( 𝑖 ∈ ∪ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ↔ ∃ 𝑢 ( 𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ) )
51 49 50 sylib ⊢ ( ( ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) ⊆ ∪ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ ( 𝑈 ∩ 𝑔 ) ) → ∃ 𝑢 ( 𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ) )
52 elinel1 ⊢ ( 𝑢 ∈ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) → 𝑢 ∈ ( 𝑈 ∩ 𝑔 ) )
53 52 elin2d ⊢ ( 𝑢 ∈ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) → 𝑢 ∈ 𝑔 )
54 elinel2 ⊢ ( 𝑢 ∈ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) → 𝑢 ∈ 𝒫 𝒫 𝑤 )
55 elpwpw ⊢ ( 𝑢 ∈ 𝒫 𝒫 𝑤 ↔ ( 𝑢 ∈ V ∧ ∪ 𝑢 ⊆ 𝑤 ) )
56 55 simprbi ⊢ ( 𝑢 ∈ 𝒫 𝒫 𝑤 → ∪ 𝑢 ⊆ 𝑤 )
57 54 56 syl ⊢ ( 𝑢 ∈ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) → ∪ 𝑢 ⊆ 𝑤 )
58 53 57 jca ⊢ ( 𝑢 ∈ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) → ( 𝑢 ∈ 𝑔 ∧ ∪ 𝑢 ⊆ 𝑤 ) )
59 58 anim2i ⊢ ( ( 𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ) → ( 𝑖 ∈ 𝑢 ∧ ( 𝑢 ∈ 𝑔 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
60 an12 ⊢ ( ( 𝑖 ∈ 𝑢 ∧ ( 𝑢 ∈ 𝑔 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ↔ ( 𝑢 ∈ 𝑔 ∧ ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
61 59 60 sylib ⊢ ( ( 𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ) → ( 𝑢 ∈ 𝑔 ∧ ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
62 61 eximi ⊢ ( ∃ 𝑢 ( 𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ) → ∃ 𝑢 ( 𝑢 ∈ 𝑔 ∧ ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
63 df-rex ⊢ ( ∃ 𝑢 ∈ 𝑔 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ↔ ∃ 𝑢 ( 𝑢 ∈ 𝑔 ∧ ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
64 62 63 sylibr ⊢ ( ∃ 𝑢 ( 𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ) → ∃ 𝑢 ∈ 𝑔 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) )
65 51 64 syl ⊢ ( ( ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) ⊆ ∪ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ ( 𝑈 ∩ 𝑔 ) ) → ∃ 𝑢 ∈ 𝑔 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) )
66 65 3expia ⊢ ( ( ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) ⊆ ∪ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ∧ 𝑖 ∈ 𝑧 ) → ( 𝑖 ∈ ∪ ( 𝑈 ∩ 𝑔 ) → ∃ 𝑢 ∈ 𝑔 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
67 44 66 syl5bi ⊢ ( ( ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) ⊆ ∪ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ∧ 𝑖 ∈ 𝑧 ) → ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔 ) → ∃ 𝑢 ∈ 𝑔 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
68 67 ralrimiva ⊢ ( ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) ⊆ ∪ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) → ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔 ) → ∃ 𝑢 ∈ 𝑔 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
69 35 68 anim12i ⊢ ( ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) ⊆ ∪ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ) → ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔 ) → ∃ 𝑢 ∈ 𝑔 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) )
70 69 reximi ⊢ ( ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ ( 𝑈 ∩ 𝑔 ) ) ⊆ ∪ ( ( 𝑈 ∩ 𝑔 ) ∩ 𝒫 𝒫 𝑤 ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔 ) → ∃ 𝑢 ∈ 𝑔 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) )
71 32 70 sylg ⊢ ( ∀ 𝑓 ∈ 𝒫 𝑈 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) → ∀ 𝑔 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔 ) → ∃ 𝑢 ∈ 𝑔 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) )
72 elequ2 ⊢ ( 𝑓 = 𝑔 → ( 𝑣 ∈ 𝑓 ↔ 𝑣 ∈ 𝑔 ) )
73 72 anbi2d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ↔ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔 ) ) )
74 73 rexbidv ⊢ ( 𝑓 = 𝑔 → ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ↔ ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔 ) ) )
75 rexeq ⊢ ( 𝑓 = 𝑔 → ( ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ↔ ∃ 𝑢 ∈ 𝑔 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
76 74 75 imbi12d ⊢ ( 𝑓 = 𝑔 → ( ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ↔ ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔 ) → ∃ 𝑢 ∈ 𝑔 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) )
77 76 ralbidv ⊢ ( 𝑓 = 𝑔 → ( ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ↔ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔 ) → ∃ 𝑢 ∈ 𝑔 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) )
78 77 anbi2d ⊢ ( 𝑓 = 𝑔 → ( ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ↔ ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔 ) → ∃ 𝑢 ∈ 𝑔 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) )
79 78 rexbidv ⊢ ( 𝑓 = 𝑔 → ( ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ↔ ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔 ) → ∃ 𝑢 ∈ 𝑔 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) )
80 79 cbvalvw ⊢ ( ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ↔ ∀ 𝑔 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔 ) → ∃ 𝑢 ∈ 𝑔 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) )
81 71 80 sylibr ⊢ ( ∀ 𝑓 ∈ 𝒫 𝑈 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) → ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) )
82 17 81 jca ⊢ ( ∀ 𝑓 ∈ 𝒫 𝑈 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) → ( 𝒫 𝑧 ⊆ 𝑈 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) )
83 nfv ⊢ Ⅎ 𝑓 𝒫 𝑧 ⊆ 𝑈
84 nfa1 ⊢ Ⅎ 𝑓 ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
85 83 84 nfan ⊢ Ⅎ 𝑓 ( 𝒫 𝑧 ⊆ 𝑈 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) )
86 elpwi ⊢ ( 𝑓 ∈ 𝒫 𝑈 → 𝑓 ⊆ 𝑈 )
87 sp ⊢ ( ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) )
88 ssin ⊢ ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝒫 𝑧 ⊆ 𝑤 ) ↔ 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) )
89 88 biimpi ⊢ ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝒫 𝑧 ⊆ 𝑤 ) → 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) )
90 89 ex ⊢ ( 𝒫 𝑧 ⊆ 𝑈 → ( 𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ) )
91 90 adantr ⊢ ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ) → ( 𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ) )
92 simp3 ⊢ ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓 ) → 𝑖 ∈ ∪ 𝑓 )
93 eluni ⊢ ( 𝑖 ∈ ∪ 𝑓 ↔ ∃ 𝑣 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) )
94 92 93 sylib ⊢ ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓 ) → ∃ 𝑣 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) )
95 simpl2 ⊢ ( ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓 ) ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → 𝑓 ⊆ 𝑈 )
96 simprr ⊢ ( ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓 ) ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → 𝑣 ∈ 𝑓 )
97 95 96 sseldd ⊢ ( ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓 ) ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → 𝑣 ∈ 𝑈 )
98 simprl ⊢ ( ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓 ) ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → 𝑖 ∈ 𝑣 )
99 97 98 96 3jca ⊢ ( ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓 ) ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) → ( 𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) )
100 99 ex ⊢ ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓 ) → ( ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ( 𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) )
101 100 eximdv ⊢ ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓 ) → ( ∃ 𝑣 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑣 ( 𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) )
102 94 101 mpd ⊢ ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓 ) → ∃ 𝑣 ( 𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) )
103 df-rex ⊢ ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ↔ ∃ 𝑣 ( 𝑣 ∈ 𝑈 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) )
104 3anass ⊢ ( ( 𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ↔ ( 𝑣 ∈ 𝑈 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) )
105 104 exbii ⊢ ( ∃ 𝑣 ( 𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ↔ ∃ 𝑣 ( 𝑣 ∈ 𝑈 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) )
106 103 105 bitr4i ⊢ ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ↔ ∃ 𝑣 ( 𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) )
107 102 106 sylibr ⊢ ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) )
108 107 3expia ⊢ ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ) → ( 𝑖 ∈ ∪ 𝑓 → ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ) )
109 elin ⊢ ( 𝑢 ∈ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ↔ ( 𝑢 ∈ 𝑓 ∧ 𝑢 ∈ 𝒫 𝒫 𝑤 ) )
110 vex ⊢ 𝑢 ∈ V
111 110 55 mpbiran ⊢ ( 𝑢 ∈ 𝒫 𝒫 𝑤 ↔ ∪ 𝑢 ⊆ 𝑤 )
112 111 anbi2i ⊢ ( ( 𝑢 ∈ 𝑓 ∧ 𝑢 ∈ 𝒫 𝒫 𝑤 ) ↔ ( 𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤 ) )
113 109 112 bitri ⊢ ( 𝑢 ∈ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ↔ ( 𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤 ) )
114 113 anbi2i ⊢ ( ( 𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ↔ ( 𝑖 ∈ 𝑢 ∧ ( 𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
115 an12 ⊢ ( ( 𝑢 ∈ 𝑓 ∧ ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ↔ ( 𝑖 ∈ 𝑢 ∧ ( 𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
116 114 115 bitr4i ⊢ ( ( 𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ↔ ( 𝑢 ∈ 𝑓 ∧ ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
117 116 exbii ⊢ ( ∃ 𝑢 ( 𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ↔ ∃ 𝑢 ( 𝑢 ∈ 𝑓 ∧ ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
118 eluni ⊢ ( 𝑖 ∈ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ↔ ∃ 𝑢 ( 𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) )
119 df-rex ⊢ ( ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ↔ ∃ 𝑢 ( 𝑢 ∈ 𝑓 ∧ ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
120 117 118 119 3bitr4i ⊢ ( 𝑖 ∈ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ↔ ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) )
121 120 biimpri ⊢ ( ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) → 𝑖 ∈ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) )
122 121 a1i ⊢ ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ) → ( ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) → 𝑖 ∈ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) )
123 108 122 imim12d ⊢ ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ) → ( ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) → ( 𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ) )
124 123 ralimdv ⊢ ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ) → ( ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) → ∀ 𝑖 ∈ 𝑧 ( 𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ) )
125 elin ⊢ ( 𝑖 ∈ ( 𝑧 ∩ ∪ 𝑓 ) ↔ ( 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ 𝑓 ) )
126 125 imbi1i ⊢ ( ( 𝑖 ∈ ( 𝑧 ∩ ∪ 𝑓 ) → 𝑖 ∈ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ↔ ( ( 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ 𝑓 ) → 𝑖 ∈ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) )
127 impexp ⊢ ( ( ( 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ 𝑓 ) → 𝑖 ∈ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ↔ ( 𝑖 ∈ 𝑧 → ( 𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ) )
128 126 127 bitri ⊢ ( ( 𝑖 ∈ ( 𝑧 ∩ ∪ 𝑓 ) → 𝑖 ∈ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ↔ ( 𝑖 ∈ 𝑧 → ( 𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ) )
129 128 albii ⊢ ( ∀ 𝑖 ( 𝑖 ∈ ( 𝑧 ∩ ∪ 𝑓 ) → 𝑖 ∈ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ↔ ∀ 𝑖 ( 𝑖 ∈ 𝑧 → ( 𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ) )
130 dfss2 ⊢ ( ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ↔ ∀ 𝑖 ( 𝑖 ∈ ( 𝑧 ∩ ∪ 𝑓 ) → 𝑖 ∈ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) )
131 df-ral ⊢ ( ∀ 𝑖 ∈ 𝑧 ( 𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ↔ ∀ 𝑖 ( 𝑖 ∈ 𝑧 → ( 𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ) )
132 129 130 131 3bitr4i ⊢ ( ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ↔ ∀ 𝑖 ∈ 𝑧 ( 𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) )
133 124 132 syl6ibr ⊢ ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ) → ( ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) → ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) )
134 91 133 anim12d ⊢ ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ) → ( ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) → ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ) )
135 134 reximdv ⊢ ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ) → ( ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ) )
136 135 3impia ⊢ ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) )
137 136 3com23 ⊢ ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ∧ 𝑓 ⊆ 𝑈 ) → ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) )
138 87 137 syl3an2 ⊢ ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ∧ 𝑓 ⊆ 𝑈 ) → ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) )
139 138 3expa ⊢ ( ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ∧ 𝑓 ⊆ 𝑈 ) → ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) )
140 86 139 sylan2 ⊢ ( ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝒫 𝑈 ) → ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) )
141 85 140 ralrimia ⊢ ( ( 𝒫 𝑧 ⊆ 𝑈 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) → ∀ 𝑓 ∈ 𝒫 𝑈 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) )
142 82 141 impbii ⊢ ( ∀ 𝑓 ∈ 𝒫 𝑈 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ ( 𝑈 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ↔ ( 𝒫 𝑧 ⊆ 𝑈 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) )