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