Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . . . . 6
⊢
((𝒫 𝑧
⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤)) → 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)) |
2 | 1 | reximi 3176 |
. . . . 5
⊢
(∃𝑤 ∈
𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤)) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)) |
3 | 2 | ralimi 3087 |
. . . 4
⊢
(∀𝑓 ∈
𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤)) → ∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)) |
4 | | 0elpw 5276 |
. . . . . . . 8
⊢ ∅
∈ 𝒫 𝑈 |
5 | 4 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ ∅ ∈ 𝒫 𝑈) |
6 | | biidd 261 |
. . . . . . 7
⊢
((⊤ ∧ 𝑓 =
∅) → (∃𝑤
∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ↔ ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))) |
7 | 5, 6 | rspcdv 3550 |
. . . . . 6
⊢ (⊤
→ (∀𝑓 ∈
𝒫 𝑈∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))) |
8 | 7 | mptru 1546 |
. . . . 5
⊢
(∀𝑓 ∈
𝒫 𝑈∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)) |
9 | | inss1 4162 |
. . . . . . 7
⊢ (𝑈 ∩ 𝑤) ⊆ 𝑈 |
10 | | sstr2 3927 |
. . . . . . 7
⊢
(𝒫 𝑧 ⊆
(𝑈 ∩ 𝑤) → ((𝑈 ∩ 𝑤) ⊆ 𝑈 → 𝒫 𝑧 ⊆ 𝑈)) |
11 | 9, 10 | mpi 20 |
. . . . . 6
⊢
(𝒫 𝑧 ⊆
(𝑈 ∩ 𝑤) → 𝒫 𝑧 ⊆ 𝑈) |
12 | 11 | reximi 3176 |
. . . . 5
⊢
(∃𝑤 ∈
𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ 𝑈) |
13 | 8, 12 | syl 17 |
. . . 4
⊢
(∀𝑓 ∈
𝒫 𝑈∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) → ∃𝑤 ∈ 𝑈 𝒫 𝑧 ⊆ 𝑈) |
14 | | rexex 3169 |
. . . . 5
⊢
(∃𝑤 ∈
𝑈 𝒫 𝑧 ⊆ 𝑈 → ∃𝑤𝒫 𝑧 ⊆ 𝑈) |
15 | | ax5e 1915 |
. . . . 5
⊢
(∃𝑤𝒫
𝑧 ⊆ 𝑈 → 𝒫 𝑧 ⊆ 𝑈) |
16 | 14, 15 | syl 17 |
. . . 4
⊢
(∃𝑤 ∈
𝑈 𝒫 𝑧 ⊆ 𝑈 → 𝒫 𝑧 ⊆ 𝑈) |
17 | 3, 13, 16 | 3syl 18 |
. . 3
⊢
(∀𝑓 ∈
𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤)) → 𝒫 𝑧 ⊆ 𝑈) |
18 | | inss1 4162 |
. . . . . . . 8
⊢ (𝑈 ∩ 𝑔) ⊆ 𝑈 |
19 | | vex 3433 |
. . . . . . . . . 10
⊢ 𝑔 ∈ V |
20 | 19 | inex2 5240 |
. . . . . . . . 9
⊢ (𝑈 ∩ 𝑔) ∈ V |
21 | 20 | elpw 4537 |
. . . . . . . 8
⊢ ((𝑈 ∩ 𝑔) ∈ 𝒫 𝑈 ↔ (𝑈 ∩ 𝑔) ⊆ 𝑈) |
22 | 18, 21 | mpbir 230 |
. . . . . . 7
⊢ (𝑈 ∩ 𝑔) ∈ 𝒫 𝑈 |
23 | | unieq 4850 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑈 ∩ 𝑔) → ∪ 𝑓 = ∪
(𝑈 ∩ 𝑔)) |
24 | 23 | ineq2d 4146 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑈 ∩ 𝑔) → (𝑧 ∩ ∪ 𝑓) = (𝑧 ∩ ∪ (𝑈 ∩ 𝑔))) |
25 | | ineq1 4139 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑈 ∩ 𝑔) → (𝑓 ∩ 𝒫 𝒫 𝑤) = ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) |
26 | 25 | unieqd 4853 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑈 ∩ 𝑔) → ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) = ∪
((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫
𝑤)) |
27 | 24, 26 | sseq12d 3953 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑈 ∩ 𝑔) → ((𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤) ↔ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪
((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫
𝑤))) |
28 | 27 | anbi2d 629 |
. . . . . . . . 9
⊢ (𝑓 = (𝑈 ∩ 𝑔) → ((𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤)) ↔ (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪
((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫
𝑤)))) |
29 | 28 | rexbidv 3224 |
. . . . . . . 8
⊢ (𝑓 = (𝑈 ∩ 𝑔) → (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤)) ↔ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪
((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫
𝑤)))) |
30 | 29 | rspcv 3554 |
. . . . . . 7
⊢ ((𝑈 ∩ 𝑔) ∈ 𝒫 𝑈 → (∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤)) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪
((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫
𝑤)))) |
31 | 22, 30 | ax-mp 5 |
. . . . . 6
⊢
(∀𝑓 ∈
𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤)) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪
((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫
𝑤))) |
32 | 31 | alrimiv 1930 |
. . . . 5
⊢
(∀𝑓 ∈
𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤)) → ∀𝑔∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪
((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫
𝑤))) |
33 | | inss2 4163 |
. . . . . . . 8
⊢ (𝑈 ∩ 𝑤) ⊆ 𝑤 |
34 | | sstr2 3927 |
. . . . . . . 8
⊢
(𝒫 𝑧 ⊆
(𝑈 ∩ 𝑤) → ((𝑈 ∩ 𝑤) ⊆ 𝑤 → 𝒫 𝑧 ⊆ 𝑤)) |
35 | 33, 34 | mpi 20 |
. . . . . . 7
⊢
(𝒫 𝑧 ⊆
(𝑈 ∩ 𝑤) → 𝒫 𝑧 ⊆ 𝑤) |
36 | | an12 642 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)) ↔ (𝑖 ∈ 𝑣 ∧ (𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔))) |
37 | | elin 3902 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ (𝑈 ∩ 𝑔) ↔ (𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔)) |
38 | 37 | bicomi 223 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔) ↔ 𝑣 ∈ (𝑈 ∩ 𝑔)) |
39 | 38 | anbi2i 623 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ 𝑣 ∧ (𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝑔)) ↔ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ (𝑈 ∩ 𝑔))) |
40 | 36, 39 | bitri 274 |
. . . . . . . . . . 11
⊢ ((𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)) ↔ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ (𝑈 ∩ 𝑔))) |
41 | 40 | exbii 1850 |
. . . . . . . . . 10
⊢
(∃𝑣(𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔)) ↔ ∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ (𝑈 ∩ 𝑔))) |
42 | | df-rex 3070 |
. . . . . . . . . 10
⊢
(∃𝑣 ∈
𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔))) |
43 | | eluni 4842 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ∪ (𝑈
∩ 𝑔) ↔
∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ (𝑈 ∩ 𝑔))) |
44 | 41, 42, 43 | 3bitr4i 303 |
. . . . . . . . 9
⊢
(∃𝑣 ∈
𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) ↔ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) |
45 | | simp1 1135 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∩ ∪ (𝑈
∩ 𝑔)) ⊆ ∪ ((𝑈
∩ 𝑔) ∩ 𝒫
𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪
((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫
𝑤)) |
46 | | elin 3902 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ↔ (𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔))) |
47 | 46 | biimpri 227 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → 𝑖 ∈ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔))) |
48 | 47 | 3adant1 1129 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∩ ∪ (𝑈
∩ 𝑔)) ⊆ ∪ ((𝑈
∩ 𝑔) ∩ 𝒫
𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → 𝑖 ∈ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔))) |
49 | 45, 48 | sseldd 3921 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∩ ∪ (𝑈
∩ 𝑔)) ⊆ ∪ ((𝑈
∩ 𝑔) ∩ 𝒫
𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → 𝑖 ∈ ∪ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) |
50 | | eluni 4842 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ∪ ((𝑈
∩ 𝑔) ∩ 𝒫
𝒫 𝑤) ↔
∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))) |
51 | 49, 50 | sylib 217 |
. . . . . . . . . . 11
⊢ (((𝑧 ∩ ∪ (𝑈
∩ 𝑔)) ⊆ ∪ ((𝑈
∩ 𝑔) ∩ 𝒫
𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → ∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤))) |
52 | | elinel1 4128 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → 𝑢 ∈ (𝑈 ∩ 𝑔)) |
53 | 52 | elin2d 4132 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → 𝑢 ∈ 𝑔) |
54 | | elinel2 4129 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → 𝑢 ∈ 𝒫 𝒫 𝑤) |
55 | | elpwpw 5030 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ 𝒫 𝒫
𝑤 ↔ (𝑢 ∈ V ∧ ∪ 𝑢
⊆ 𝑤)) |
56 | 55 | simprbi 497 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ 𝒫 𝒫
𝑤 → ∪ 𝑢
⊆ 𝑤) |
57 | 54, 56 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → ∪ 𝑢
⊆ 𝑤) |
58 | 53, 57 | jca 512 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤) → (𝑢 ∈ 𝑔 ∧ ∪ 𝑢 ⊆ 𝑤)) |
59 | 58 | anim2i 617 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → (𝑖 ∈ 𝑢 ∧ (𝑢 ∈ 𝑔 ∧ ∪ 𝑢 ⊆ 𝑤))) |
60 | | an12 642 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ 𝑢 ∧ (𝑢 ∈ 𝑔 ∧ ∪ 𝑢 ⊆ 𝑤)) ↔ (𝑢 ∈ 𝑔 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
61 | 59, 60 | sylib 217 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → (𝑢 ∈ 𝑔 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
62 | 61 | eximi 1837 |
. . . . . . . . . . . 12
⊢
(∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → ∃𝑢(𝑢 ∈ 𝑔 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
63 | | df-rex 3070 |
. . . . . . . . . . . 12
⊢
(∃𝑢 ∈
𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢(𝑢 ∈ 𝑔 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
64 | 62, 63 | sylibr 233 |
. . . . . . . . . . 11
⊢
(∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ ((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫 𝑤)) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) |
65 | 51, 64 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑧 ∩ ∪ (𝑈
∩ 𝑔)) ⊆ ∪ ((𝑈
∩ 𝑔) ∩ 𝒫
𝒫 𝑤) ∧ 𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ (𝑈 ∩ 𝑔)) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) |
66 | 65 | 3expia 1120 |
. . . . . . . . 9
⊢ (((𝑧 ∩ ∪ (𝑈
∩ 𝑔)) ⊆ ∪ ((𝑈
∩ 𝑔) ∩ 𝒫
𝒫 𝑤) ∧ 𝑖 ∈ 𝑧) → (𝑖 ∈ ∪ (𝑈 ∩ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
67 | 44, 66 | syl5bi 241 |
. . . . . . . 8
⊢ (((𝑧 ∩ ∪ (𝑈
∩ 𝑔)) ⊆ ∪ ((𝑈
∩ 𝑔) ∩ 𝒫
𝒫 𝑤) ∧ 𝑖 ∈ 𝑧) → (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
68 | 67 | ralrimiva 3108 |
. . . . . . 7
⊢ ((𝑧 ∩ ∪ (𝑈
∩ 𝑔)) ⊆ ∪ ((𝑈
∩ 𝑔) ∩ 𝒫
𝒫 𝑤) →
∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
69 | 35, 68 | anim12i 613 |
. . . . . 6
⊢
((𝒫 𝑧
⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪
((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫
𝑤)) → (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) |
70 | 69 | reximi 3176 |
. . . . 5
⊢
(∃𝑤 ∈
𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ (𝑈 ∩ 𝑔)) ⊆ ∪
((𝑈 ∩ 𝑔) ∩ 𝒫 𝒫
𝑤)) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) |
71 | 32, 70 | sylg 1825 |
. . . 4
⊢
(∀𝑓 ∈
𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤)) → ∀𝑔∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) |
72 | | elequ2 2121 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → (𝑣 ∈ 𝑓 ↔ 𝑣 ∈ 𝑔)) |
73 | 72 | anbi2d 629 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → ((𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔))) |
74 | 73 | rexbidv 3224 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ ∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔))) |
75 | | rexeq 3341 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → (∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
76 | 74, 75 | imbi12d 345 |
. . . . . . . 8
⊢ (𝑓 = 𝑔 → ((∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ↔ (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) |
77 | 76 | ralbidv 3121 |
. . . . . . 7
⊢ (𝑓 = 𝑔 → (∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ↔ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) |
78 | 77 | anbi2d 629 |
. . . . . 6
⊢ (𝑓 = 𝑔 → ((𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ↔ (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))) |
79 | 78 | rexbidv 3224 |
. . . . 5
⊢ (𝑓 = 𝑔 → (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ↔ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))) |
80 | 79 | cbvalvw 2039 |
. . . 4
⊢
(∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ↔ ∀𝑔∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑔) → ∃𝑢 ∈ 𝑔 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) |
81 | 71, 80 | sylibr 233 |
. . 3
⊢
(∀𝑓 ∈
𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤)) → ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) |
82 | 17, 81 | jca 512 |
. 2
⊢
(∀𝑓 ∈
𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤)) → (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))) |
83 | | nfv 1917 |
. . . 4
⊢
Ⅎ𝑓𝒫
𝑧 ⊆ 𝑈 |
84 | | nfa1 2148 |
. . . 4
⊢
Ⅎ𝑓∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
85 | 83, 84 | nfan 1902 |
. . 3
⊢
Ⅎ𝑓(𝒫
𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) |
86 | | elpwi 4542 |
. . . 4
⊢ (𝑓 ∈ 𝒫 𝑈 → 𝑓 ⊆ 𝑈) |
87 | | sp 2176 |
. . . . . 6
⊢
(∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) |
88 | | ssin 4164 |
. . . . . . . . . . . . 13
⊢
((𝒫 𝑧
⊆ 𝑈 ∧ 𝒫
𝑧 ⊆ 𝑤) ↔ 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)) |
89 | 88 | biimpi 215 |
. . . . . . . . . . . 12
⊢
((𝒫 𝑧
⊆ 𝑈 ∧ 𝒫
𝑧 ⊆ 𝑤) → 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤)) |
90 | 89 | ex 413 |
. . . . . . . . . . 11
⊢
(𝒫 𝑧 ⊆
𝑈 → (𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))) |
91 | 90 | adantr 481 |
. . . . . . . . . 10
⊢
((𝒫 𝑧
⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (𝒫 𝑧 ⊆ 𝑤 → 𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤))) |
92 | | simp3 1137 |
. . . . . . . . . . . . . . . . 17
⊢
((𝒫 𝑧
⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → 𝑖 ∈ ∪ 𝑓) |
93 | | eluni 4842 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ∪ 𝑓
↔ ∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) |
94 | 92, 93 | sylib 217 |
. . . . . . . . . . . . . . . 16
⊢
((𝒫 𝑧
⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → ∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) |
95 | | simpl2 1191 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((𝒫 𝑧
⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → 𝑓 ⊆ 𝑈) |
96 | | simprr 770 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((𝒫 𝑧
⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → 𝑣 ∈ 𝑓) |
97 | 95, 96 | sseldd 3921 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((𝒫 𝑧
⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → 𝑣 ∈ 𝑈) |
98 | | simprl 768 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((𝒫 𝑧
⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → 𝑖 ∈ 𝑣) |
99 | 97, 98, 96 | 3jca 1127 |
. . . . . . . . . . . . . . . . . 18
⊢
(((𝒫 𝑧
⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) → (𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) |
100 | 99 | ex 413 |
. . . . . . . . . . . . . . . . 17
⊢
((𝒫 𝑧
⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → ((𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → (𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))) |
101 | 100 | eximdv 1920 |
. . . . . . . . . . . . . . . 16
⊢
((𝒫 𝑧
⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → (∃𝑣(𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))) |
102 | 94, 101 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢
((𝒫 𝑧
⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → ∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) |
103 | | df-rex 3070 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑣 ∈
𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))) |
104 | | 3anass 1094 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ (𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))) |
105 | 104 | exbii 1850 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))) |
106 | 103, 105 | bitr4i 277 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑣 ∈
𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) |
107 | 102, 106 | sylibr 233 |
. . . . . . . . . . . . . 14
⊢
((𝒫 𝑧
⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ 𝑖 ∈ ∪ 𝑓) → ∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓)) |
108 | 107 | 3expia 1120 |
. . . . . . . . . . . . 13
⊢
((𝒫 𝑧
⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (𝑖 ∈ ∪ 𝑓 → ∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓))) |
109 | | elin 3902 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ (𝑢 ∈ 𝑓 ∧ 𝑢 ∈ 𝒫 𝒫 𝑤)) |
110 | | vex 3433 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑢 ∈ V |
111 | 110, 55 | mpbiran 706 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈ 𝒫 𝒫
𝑤 ↔ ∪ 𝑢
⊆ 𝑤) |
112 | 111 | anbi2i 623 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑢 ∈ 𝑓 ∧ 𝑢 ∈ 𝒫 𝒫 𝑤) ↔ (𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤)) |
113 | 109, 112 | bitri 274 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ (𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤)) |
114 | 113 | anbi2i 623 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ 𝑢 ∧ 𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑖 ∈ 𝑢 ∧ (𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤))) |
115 | | an12 642 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ 𝑓 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) ↔ (𝑖 ∈ 𝑢 ∧ (𝑢 ∈ 𝑓 ∧ ∪ 𝑢 ⊆ 𝑤))) |
116 | 114, 115 | bitr4i 277 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ 𝑢 ∧ 𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑢 ∈ 𝑓 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
117 | 116 | exbii 1850 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∃𝑢(𝑢 ∈ 𝑓 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
118 | | eluni 4842 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ∪ (𝑓
∩ 𝒫 𝒫 𝑤) ↔ ∃𝑢(𝑖 ∈ 𝑢 ∧ 𝑢 ∈ (𝑓 ∩ 𝒫 𝒫 𝑤))) |
119 | | df-rex 3070 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑢 ∈
𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢(𝑢 ∈ 𝑓 ∧ (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) |
120 | 117, 118,
119 | 3bitr4i 303 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ∪ (𝑓
∩ 𝒫 𝒫 𝑤) ↔ ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) |
121 | 120 | biimpri 227 |
. . . . . . . . . . . . . 14
⊢
(∃𝑢 ∈
𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) |
122 | 121 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((𝒫 𝑧
⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))) |
123 | 108, 122 | imim12d 81 |
. . . . . . . . . . . 12
⊢
((𝒫 𝑧
⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → ((∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))) |
124 | 123 | ralimdv 3104 |
. . . . . . . . . . 11
⊢
((𝒫 𝑧
⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → ∀𝑖 ∈ 𝑧 (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))) |
125 | | elin 3902 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑧 ∩ ∪ 𝑓) ↔ (𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ 𝑓)) |
126 | 125 | imbi1i 350 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (𝑧 ∩ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ((𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))) |
127 | | impexp 451 |
. . . . . . . . . . . . . 14
⊢ (((𝑖 ∈ 𝑧 ∧ 𝑖 ∈ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑖 ∈ 𝑧 → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))) |
128 | 126, 127 | bitri 274 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∈ (𝑧 ∩ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ (𝑖 ∈ 𝑧 → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))) |
129 | 128 | albii 1822 |
. . . . . . . . . . . 12
⊢
(∀𝑖(𝑖 ∈ (𝑧 ∩ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∀𝑖(𝑖 ∈ 𝑧 → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))) |
130 | | dfss2 3906 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∩ ∪ 𝑓)
⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∀𝑖(𝑖 ∈ (𝑧 ∩ ∪ 𝑓) → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))) |
131 | | df-ral 3069 |
. . . . . . . . . . . 12
⊢
(∀𝑖 ∈
𝑧 (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)) ↔ ∀𝑖(𝑖 ∈ 𝑧 → (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤)))) |
132 | 129, 130,
131 | 3bitr4i 303 |
. . . . . . . . . . 11
⊢ ((𝑧 ∩ ∪ 𝑓)
⊆ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤) ↔ ∀𝑖 ∈ 𝑧 (𝑖 ∈ ∪ 𝑓 → 𝑖 ∈ ∪ (𝑓 ∩ 𝒫 𝒫 𝑤))) |
133 | 124, 132 | syl6ibr 251 |
. . . . . . . . . 10
⊢
((𝒫 𝑧
⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤))) |
134 | 91, 133 | anim12d 609 |
. . . . . . . . 9
⊢
((𝒫 𝑧
⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → ((𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) → (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤)))) |
135 | 134 | reximdv 3200 |
. . . . . . . 8
⊢
((𝒫 𝑧
⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈) → (∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤)))) |
136 | 135 | 3impia 1116 |
. . . . . . 7
⊢
((𝒫 𝑧
⊆ 𝑈 ∧ 𝑓 ⊆ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤))) |
137 | 136 | 3com23 1125 |
. . . . . 6
⊢
((𝒫 𝑧
⊆ 𝑈 ∧
∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ∧ 𝑓 ⊆ 𝑈) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤))) |
138 | 87, 137 | syl3an2 1163 |
. . . . 5
⊢
((𝒫 𝑧
⊆ 𝑈 ∧
∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))) ∧ 𝑓 ⊆ 𝑈) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤))) |
139 | 138 | 3expa 1117 |
. . . 4
⊢
(((𝒫 𝑧
⊆ 𝑈 ∧
∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ∧ 𝑓 ⊆ 𝑈) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤))) |
140 | 86, 139 | sylan2 593 |
. . 3
⊢
(((𝒫 𝑧
⊆ 𝑈 ∧
∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ∧ 𝑓 ∈ 𝒫 𝑈) → ∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤))) |
141 | 85, 140 | ralrimia 3427 |
. 2
⊢
((𝒫 𝑧
⊆ 𝑈 ∧
∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∀𝑓 ∈ 𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤))) |
142 | 82, 141 | impbii 208 |
1
⊢
(∀𝑓 ∈
𝒫 𝑈∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ (𝑈 ∩ 𝑤) ∧ (𝑧 ∩ ∪ 𝑓) ⊆ ∪ (𝑓
∩ 𝒫 𝒫 𝑤)) ↔ (𝒫 𝑧 ⊆ 𝑈 ∧ ∀𝑓∃𝑤 ∈ 𝑈 (𝒫 𝑧 ⊆ 𝑤 ∧ ∀𝑖 ∈ 𝑧 (∃𝑣 ∈ 𝑈 (𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓) → ∃𝑢 ∈ 𝑓 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))) |