Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶ℝ → 𝐹:𝐴⟶ℝ) |
2 | 1 | feqmptd 6593 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶ℝ → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
3 | 2 | cnveqd 5624 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶ℝ → ◡𝐹 = ◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
4 | 3 | imaeq1d 5797 |
. . . . . . 7
⊢ (𝐹:𝐴⟶ℝ → (◡𝐹 “ 𝑏) = (◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) “ 𝑏)) |
5 | 4 | ad2antrr 722 |
. . . . . 6
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) → (◡𝐹 “ 𝑏) = (◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) “ 𝑏)) |
6 | | exmid 887 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ ((((topGen‘ran
(,)) ↾t 𝐴)
CnP (topGen‘ran (,)))‘𝑥) ∨ ¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)) |
7 | 6 | biantrur 531 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ 𝑏 ↔ ((𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∨ ¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)) ∧ (𝐹‘𝑥) ∈ 𝑏)) |
8 | | andir 1001 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ ((((topGen‘ran
(,)) ↾t 𝐴)
CnP (topGen‘ran (,)))‘𝑥) ∨ ¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)) ∧ (𝐹‘𝑥) ∈ 𝑏) ↔ ((𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏) ∨ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏))) |
9 | 7, 8 | bitri 276 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) ∈ 𝑏 ↔ ((𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏) ∨ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏))) |
10 | | retopbas 23040 |
. . . . . . . . . . . . . . . . . 18
⊢ ran (,)
∈ TopBases |
11 | | bastg 21246 |
. . . . . . . . . . . . . . . . . 18
⊢ (ran (,)
∈ TopBases → ran (,) ⊆ (topGen‘ran (,))) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ran (,)
⊆ (topGen‘ran (,)) |
13 | 12 | sseli 3880 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ ran (,) → 𝑏 ∈ (topGen‘ran
(,))) |
14 | 13 | ad2antlr 723 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) → 𝑏 ∈ (topGen‘ran
(,))) |
15 | | cnpimaex 21536 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ ((((topGen‘ran
(,)) ↾t 𝐴)
CnP (topGen‘ran (,)))‘𝑥) ∧ 𝑏 ∈ (topGen‘ran (,)) ∧ (𝐹‘𝑥) ∈ 𝑏) → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) |
16 | 15 | 3com12 1114 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 ∈ (topGen‘ran (,))
∧ 𝐹 ∈
((((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏) → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) |
17 | 16 | 3expa 1109 |
. . . . . . . . . . . . . . 15
⊢ (((𝑏 ∈ (topGen‘ran (,))
∧ 𝐹 ∈
((((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,)))‘𝑥)) ∧ (𝐹‘𝑥) ∈ 𝑏) → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) |
18 | 14, 17 | sylanl1 676 |
. . . . . . . . . . . . . 14
⊢
((((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) ∧ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)) ∧ (𝐹‘𝑥) ∈ 𝑏) → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) |
19 | 18 | ex 413 |
. . . . . . . . . . . . 13
⊢
(((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) ∧ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)) → ((𝐹‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))) |
20 | | simprrr 778 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ (𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))) → (𝐹 “ 𝑦) ⊆ 𝑏) |
21 | | ffn 6374 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:𝐴⟶ℝ → 𝐹 Fn 𝐴) |
22 | 21 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → 𝐹 Fn 𝐴) |
23 | | restsspw 16522 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((topGen‘ran (,)) ↾t 𝐴) ⊆ 𝒫 𝐴 |
24 | 23 | sseli 3880 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
→ 𝑦 ∈ 𝒫
𝐴) |
25 | 24 | elpwid 4459 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
→ 𝑦 ⊆ 𝐴) |
26 | | simpl 483 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏) → 𝑥 ∈ 𝑦) |
27 | | fnfvima 6851 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ 𝑥 ∈ 𝑦) → (𝐹‘𝑥) ∈ (𝐹 “ 𝑦)) |
28 | 22, 25, 26, 27 | syl3an 1151 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) → (𝐹‘𝑥) ∈ (𝐹 “ 𝑦)) |
29 | 28 | 3expb 1111 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ (𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))) → (𝐹‘𝑥) ∈ (𝐹 “ 𝑦)) |
30 | 20, 29 | sseldd 3885 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ (𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))) → (𝐹‘𝑥) ∈ 𝑏) |
31 | 30 | rexlimdvaa 3245 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏) → (𝐹‘𝑥) ∈ 𝑏)) |
32 | 31 | ad3antrrr 726 |
. . . . . . . . . . . . 13
⊢
(((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) ∧ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)) → (∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏) → (𝐹‘𝑥) ∈ 𝑏)) |
33 | 19, 32 | impbid 213 |
. . . . . . . . . . . 12
⊢
(((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) ∧ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)) → ((𝐹‘𝑥) ∈ 𝑏 ↔ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))) |
34 | 33 | pm5.32da 579 |
. . . . . . . . . . 11
⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏) ↔ (𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)))) |
35 | | r19.42v 3308 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
((topGen‘ran (,)) ↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) ↔ (𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))) |
36 | 34, 35 | syl6bbr 290 |
. . . . . . . . . 10
⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏) ↔ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)))) |
37 | 36 | orbi1d 909 |
. . . . . . . . 9
⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) → (((𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏) ∨ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)) ↔ (∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) ∨ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)))) |
38 | 9, 37 | syl5bb 284 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) ∈ 𝑏 ↔ (∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) ∨ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)))) |
39 | 38 | rabbidva 3419 |
. . . . . . 7
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) → {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ 𝑏} = {𝑥 ∈ 𝐴 ∣ (∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) ∨ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏))}) |
40 | | eqid 2793 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) |
41 | 40 | mptpreima 5959 |
. . . . . . 7
⊢ (◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) “ 𝑏) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ 𝑏} |
42 | | unrab 4189 |
. . . . . . 7
⊢ ({𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∪ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}) = {𝑥 ∈ 𝐴 ∣ (∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) ∨ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏))} |
43 | 39, 41, 42 | 3eqtr4g 2854 |
. . . . . 6
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) → (◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) “ 𝑏) = ({𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∪ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)})) |
44 | 5, 43 | eqtrd 2829 |
. . . . 5
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) → (◡𝐹 “ 𝑏) = ({𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∪ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)})) |
45 | 44 | 3adantl3 1159 |
. . . 4
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) = 0) ∧ 𝑏 ∈ ran (,)) → (◡𝐹 “ 𝑏) = ({𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∪ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)})) |
46 | | incom 4094 |
. . . . . . . . 9
⊢ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∩ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) = ({𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)} ∩ ∪
𝑦 ∈ ((topGen‘ran
(,)) ↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)}) |
47 | | dfin4 4159 |
. . . . . . . . 9
⊢ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∩ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) = (∪
𝑦 ∈ ((topGen‘ran
(,)) ↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)})) |
48 | | inrab 4190 |
. . . . . . . . . . . 12
⊢ ({𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)} ∩ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)}) = {𝑥 ∈ 𝐴 ∣ (𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} |
49 | 48 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
→ ({𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)} ∩ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)}) = {𝑥 ∈ 𝐴 ∣ (𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))}) |
50 | 49 | iuneq2i 4839 |
. . . . . . . . . 10
⊢ ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)({𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)} ∩ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)}) = ∪
𝑦 ∈ ((topGen‘ran
(,)) ↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} |
51 | | iunin2 4886 |
. . . . . . . . . 10
⊢ ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)({𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)} ∩ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)}) = ({𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)} ∩ ∪
𝑦 ∈ ((topGen‘ran
(,)) ↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)}) |
52 | | iunrab 4869 |
. . . . . . . . . 10
⊢ ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} |
53 | 50, 51, 52 | 3eqtr3i 2825 |
. . . . . . . . 9
⊢ ({𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)} ∩ ∪
𝑦 ∈ ((topGen‘ran
(,)) ↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)}) = {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} |
54 | 46, 47, 53 | 3eqtr3i 2825 |
. . . . . . . 8
⊢ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)})) = {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} |
55 | | eqeq2 2804 |
. . . . . . . . . . . . 13
⊢ (𝑦 = if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) → ({𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = 𝑦 ↔ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅))) |
56 | | eqeq2 2804 |
. . . . . . . . . . . . 13
⊢ (∅
= if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) → ({𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = ∅ ↔ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅))) |
57 | | simprrl 777 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝐹 “ 𝑦) ⊆ 𝑏) ∧ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))) → 𝑥 ∈ 𝑦) |
58 | 25 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝐹 “ 𝑦) ⊆ 𝑏) → 𝑦 ⊆ 𝐴) |
59 | 58 | sselda 3884 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝐹 “ 𝑦) ⊆ 𝑏) ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴) |
60 | | pm3.22 460 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 “ 𝑦) ⊆ 𝑏 ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) |
61 | 60 | adantll 710 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝐹 “ 𝑦) ⊆ 𝑏) ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) |
62 | 59, 61 | jca 512 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝐹 “ 𝑦) ⊆ 𝑏) ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))) |
63 | 57, 62 | impbida 797 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝐹 “ 𝑦) ⊆ 𝑏) → ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) ↔ 𝑥 ∈ 𝑦)) |
64 | 63 | abbidv 2858 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝐹 “ 𝑦) ⊆ 𝑏) → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} = {𝑥 ∣ 𝑥 ∈ 𝑦}) |
65 | | df-rab 3112 |
. . . . . . . . . . . . . 14
⊢ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} |
66 | | cvjust 2788 |
. . . . . . . . . . . . . 14
⊢ 𝑦 = {𝑥 ∣ 𝑥 ∈ 𝑦} |
67 | 64, 65, 66 | 3eqtr4g 2854 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝐹 “ 𝑦) ⊆ 𝑏) → {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = 𝑦) |
68 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏) → (𝐹 “ 𝑦) ⊆ 𝑏) |
69 | 68 | con3i 157 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝐹 “ 𝑦) ⊆ 𝑏 → ¬ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) |
70 | 69 | ralrimivw 3148 |
. . . . . . . . . . . . . . 15
⊢ (¬
(𝐹 “ 𝑦) ⊆ 𝑏 → ∀𝑥 ∈ 𝐴 ¬ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) |
71 | | rabeq0 4252 |
. . . . . . . . . . . . . . 15
⊢ ({𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) |
72 | 70, 71 | sylibr 235 |
. . . . . . . . . . . . . 14
⊢ (¬
(𝐹 “ 𝑦) ⊆ 𝑏 → {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = ∅) |
73 | 72 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ ¬ (𝐹 “
𝑦) ⊆ 𝑏) → {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = ∅) |
74 | 55, 56, 67, 73 | ifbothda 4412 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
→ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅)) |
75 | 74 | iuneq2i 4839 |
. . . . . . . . . . 11
⊢ ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = ∪
𝑦 ∈ ((topGen‘ran
(,)) ↾t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) |
76 | | retop 23041 |
. . . . . . . . . . . . . 14
⊢
(topGen‘ran (,)) ∈ Top |
77 | | resttop 21440 |
. . . . . . . . . . . . . 14
⊢
(((topGen‘ran (,)) ∈ Top ∧ 𝐴 ∈ dom vol) → ((topGen‘ran
(,)) ↾t 𝐴)
∈ Top) |
78 | 76, 77 | mpan 686 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom vol →
((topGen‘ran (,)) ↾t 𝐴) ∈ Top) |
79 | | 0opn 21184 |
. . . . . . . . . . . . . . . 16
⊢
(((topGen‘ran (,)) ↾t 𝐴) ∈ Top → ∅ ∈
((topGen‘ran (,)) ↾t 𝐴)) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom vol → ∅
∈ ((topGen‘ran (,)) ↾t 𝐴)) |
81 | | ifcl 4419 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ ∅ ∈ ((topGen‘ran (,)) ↾t 𝐴)) → if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,))
↾t 𝐴)) |
82 | 81 | ancoms 459 |
. . . . . . . . . . . . . . 15
⊢ ((∅
∈ ((topGen‘ran (,)) ↾t 𝐴) ∧ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴))
→ if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,))
↾t 𝐴)) |
83 | 80, 82 | sylan 580 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ dom vol ∧ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴))
→ if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,))
↾t 𝐴)) |
84 | 83 | ralrimiva 3147 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom vol →
∀𝑦 ∈
((topGen‘ran (,)) ↾t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,))
↾t 𝐴)) |
85 | | iunopn 21178 |
. . . . . . . . . . . . 13
⊢
((((topGen‘ran (,)) ↾t 𝐴) ∈ Top ∧ ∀𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,))
↾t 𝐴))
→ ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,))
↾t 𝐴)) |
86 | 78, 84, 85 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom vol → ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,))
↾t 𝐴)) |
87 | | eqid 2793 |
. . . . . . . . . . . . 13
⊢
((topGen‘ran (,)) ↾t 𝐴) = ((topGen‘ran (,))
↾t 𝐴) |
88 | 87 | subopnmbl 23876 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ dom vol ∧ ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,))
↾t 𝐴))
→ ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ dom vol) |
89 | 86, 88 | mpdan 683 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom vol → ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ dom vol) |
90 | 75, 89 | syl5eqel 2885 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom vol → ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∈ dom vol) |
91 | 90 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom vol ∧
(vol*‘(𝐴 ∖
((◡(((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∈ dom vol) |
92 | | difss 4024 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ⊆ ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} |
93 | | ssrab2 3972 |
. . . . . . . . . . . . . . 15
⊢ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ⊆ 𝐴 |
94 | 93 | rgenw 3115 |
. . . . . . . . . . . . . 14
⊢
∀𝑦 ∈
((topGen‘ran (,)) ↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ⊆ 𝐴 |
95 | | iunss 4862 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ⊆ 𝐴 ↔ ∀𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ⊆ 𝐴) |
96 | 94, 95 | mpbir 232 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ⊆ 𝐴 |
97 | 92, 96 | sstri 3893 |
. . . . . . . . . . . 12
⊢ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ⊆ 𝐴 |
98 | | mblss 23803 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
99 | 97, 98 | syl5ss 3895 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom vol → (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ⊆ ℝ) |
100 | 99 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom vol ∧
(vol*‘(𝐴 ∖
((◡(((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ⊆ ℝ) |
101 | | ssdif 4032 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ⊆ 𝐴 → (∪
𝑦 ∈ ((topGen‘ran
(,)) ↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ⊆ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)})) |
102 | 96, 101 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ⊆ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) |
103 | | ovex 7039 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℝ
↑𝑚 𝐴) ∈ V |
104 | 103 | rabex 5119 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑓 ∈ (ℝ
↑𝑚 𝐴) ∣ ∀𝑏 ∈ (topGen‘ran (,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))} ∈ V |
105 | | eqid 2793 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝐴 ↦ {𝑓 ∈ (ℝ ↑𝑚
𝐴) ∣ ∀𝑏 ∈ (topGen‘ran
(,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))}) = (𝑥 ∈ 𝐴 ↦ {𝑓 ∈ (ℝ ↑𝑚
𝐴) ∣ ∀𝑏 ∈ (topGen‘ran
(,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))}) |
106 | 104, 105 | fnmpti 6351 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐴 ↦ {𝑓 ∈ (ℝ ↑𝑚
𝐴) ∣ ∀𝑏 ∈ (topGen‘ran
(,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))}) Fn 𝐴 |
107 | | retopon 23043 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
108 | | resttopon 21441 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ 𝐴 ⊆ ℝ) →
((topGen‘ran (,)) ↾t 𝐴) ∈ (TopOn‘𝐴)) |
109 | 107, 98, 108 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ dom vol →
((topGen‘ran (,)) ↾t 𝐴) ∈ (TopOn‘𝐴)) |
110 | | cnpfval 21514 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((topGen‘ran (,)) ↾t 𝐴) ∈ (TopOn‘𝐴) ∧ (topGen‘ran (,)) ∈
(TopOn‘ℝ)) → (((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) = (𝑥 ∈ 𝐴 ↦ {𝑓 ∈ (ℝ ↑𝑚
𝐴) ∣ ∀𝑏 ∈ (topGen‘ran
(,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))})) |
111 | 109, 107,
110 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ dom vol →
(((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,))) = (𝑥 ∈ 𝐴 ↦ {𝑓 ∈ (ℝ ↑𝑚
𝐴) ∣ ∀𝑏 ∈ (topGen‘ran
(,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))})) |
112 | 111 | fneq1d 6308 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ dom vol →
((((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,))) Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ {𝑓 ∈ (ℝ ↑𝑚
𝐴) ∣ ∀𝑏 ∈ (topGen‘ran
(,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))}) Fn 𝐴)) |
113 | 106, 112 | mpbiri 259 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ dom vol →
(((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,))) Fn 𝐴) |
114 | | elpreima 6684 |
. . . . . . . . . . . . . . . . . 18
⊢
((((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,))) Fn 𝐴 → (𝑥 ∈ (◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) “ ( E “ {𝐹})) ↔ (𝑥 ∈ 𝐴 ∧ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹})))) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ dom vol → (𝑥 ∈ (◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) “ ( E “ {𝐹})) ↔ (𝑥 ∈ 𝐴 ∧ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹})))) |
116 | | rele 5577 |
. . . . . . . . . . . . . . . . . . . 20
⊢ Rel
E |
117 | | elrelimasn 5821 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Rel E
→ (((((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹}) ↔ 𝐹 E ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥))) |
118 | 116, 117 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹}) ↔ 𝐹 E ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)) |
119 | | fvex 6543 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∈ V |
120 | 119 | epeli 5348 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 E ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ↔ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)) |
121 | 118, 120 | bitr2i 277 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ ((((topGen‘ran
(,)) ↾t 𝐴)
CnP (topGen‘ran (,)))‘𝑥) ↔ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹})) |
122 | 121 | anbi2i 622 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹}))) |
123 | 115, 122 | syl6rbbr 291 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ dom vol → ((𝑥 ∈ 𝐴 ∧ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)) ↔ 𝑥 ∈ (◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) “ ( E “ {𝐹})))) |
124 | 123 | abbidv 2858 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom vol → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥))} = {𝑥 ∣ 𝑥 ∈ (◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) “ ( E “ {𝐹}))}) |
125 | | df-rab 3112 |
. . . . . . . . . . . . . . 15
⊢ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥))} |
126 | | imaco 5971 |
. . . . . . . . . . . . . . . 16
⊢ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}) = (◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) “ ( E “ {𝐹})) |
127 | | abid2 2924 |
. . . . . . . . . . . . . . . 16
⊢ {𝑥 ∣ 𝑥 ∈ (◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) “ ( E “ {𝐹}))} = (◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) “ ( E “ {𝐹})) |
128 | 126, 127 | eqtr4i 2820 |
. . . . . . . . . . . . . . 15
⊢ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}) = {𝑥 ∣ 𝑥 ∈ (◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) “ ( E “ {𝐹}))} |
129 | 124, 125,
128 | 3eqtr4g 2854 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom vol → {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)} = ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) |
130 | 129 | difeq2d 4015 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom vol → (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) = (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) |
131 | 102, 130 | sseqtrid 3935 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom vol → (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ⊆ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) |
132 | | difss 4024 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) ⊆ 𝐴 |
133 | 132, 98 | syl5ss 3895 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom vol → (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) ⊆ ℝ) |
134 | 131, 133 | jca 512 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom vol →
((∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ⊆ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) ∧ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) ⊆ ℝ)) |
135 | | ovolssnul 23759 |
. . . . . . . . . . . 12
⊢
(((∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ⊆ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) ∧ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) ⊆ ℝ ∧ (vol*‘(𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) = 0) → (vol*‘(∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)})) = 0) |
136 | 135 | 3expa 1109 |
. . . . . . . . . . 11
⊢
((((∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ⊆ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) ∧ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) ⊆ ℝ) ∧
(vol*‘(𝐴 ∖
((◡(((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → (vol*‘(∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)})) = 0) |
137 | 134, 136 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom vol ∧
(vol*‘(𝐴 ∖
((◡(((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → (vol*‘(∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)})) = 0) |
138 | | nulmbl 23807 |
. . . . . . . . . 10
⊢
(((∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ⊆ ℝ ∧
(vol*‘(∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)})) = 0) → (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ∈ dom vol) |
139 | 100, 137,
138 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom vol ∧
(vol*‘(𝐴 ∖
((◡(((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ∈ dom vol) |
140 | | difmbl 23815 |
. . . . . . . . 9
⊢
((∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∈ dom vol ∧ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ∈ dom vol) → (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)})) ∈ dom vol) |
141 | 91, 139, 140 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧
(vol*‘(𝐴 ∖
((◡(((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)})) ∈ dom vol) |
142 | 54, 141 | syl5eqelr 2886 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧
(vol*‘(𝐴 ∖
((◡(((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∈ dom vol) |
143 | | ssrab2 3972 |
. . . . . . . . . 10
⊢ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ 𝐴 |
144 | 143, 98 | syl5ss 3895 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom vol → {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ ℝ) |
145 | 144 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧
(vol*‘(𝐴 ∖
((◡(((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ ℝ) |
146 | 126 | eleq2i 2872 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}) ↔ 𝑥 ∈ (◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) “ ( E “ {𝐹}))) |
147 | | ibar 529 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝐴 → (((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹}) ↔ (𝑥 ∈ 𝐴 ∧ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹})))) |
148 | 121, 147 | syl5rbb 285 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ∧ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹})) ↔ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥))) |
149 | 115, 148 | sylan9bb 510 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ (◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) “ ( E “ {𝐹})) ↔ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥))) |
150 | 146, 149 | syl5rbb 285 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ∈ 𝐴) → (𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ↔ 𝑥 ∈ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) |
151 | 150 | notbid 319 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ∈ 𝐴) → (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ↔ ¬ 𝑥 ∈ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) |
152 | 151 | biimpd 230 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ∈ 𝐴) → (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) → ¬ 𝑥 ∈ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) |
153 | 152 | adantrd 492 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ∈ 𝐴) → ((¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏) → ¬ 𝑥 ∈ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) |
154 | 153 | ss2rabdv 3968 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom vol → {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})}) |
155 | | dfdif2 3863 |
. . . . . . . . . . 11
⊢ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})} |
156 | 154, 155 | syl6sseqr 3934 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom vol → {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) |
157 | 156, 133 | jca 512 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom vol → ({𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) ∧ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) ⊆ ℝ)) |
158 | | ovolssnul 23759 |
. . . . . . . . . 10
⊢ (({𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) ∧ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) ⊆ ℝ ∧ (vol*‘(𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) = 0) → (vol*‘{𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}) = 0) |
159 | 158 | 3expa 1109 |
. . . . . . . . 9
⊢ ((({𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) ∧ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) ⊆ ℝ) ∧
(vol*‘(𝐴 ∖
((◡(((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → (vol*‘{𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}) = 0) |
160 | 157, 159 | sylan 580 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧
(vol*‘(𝐴 ∖
((◡(((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → (vol*‘{𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}) = 0) |
161 | | nulmbl 23807 |
. . . . . . . 8
⊢ (({𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ ℝ ∧ (vol*‘{𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}) = 0) → {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ∈ dom vol) |
162 | 145, 160,
161 | syl2anc 584 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧
(vol*‘(𝐴 ∖
((◡(((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ∈ dom vol) |
163 | | unmbl 23809 |
. . . . . . 7
⊢ (({𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∈ dom vol ∧ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ∈ dom vol) → ({𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∪ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}) ∈ dom vol) |
164 | 142, 162,
163 | syl2anc 584 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧
(vol*‘(𝐴 ∖
((◡(((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → ({𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∪ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}) ∈ dom vol) |
165 | 164 | 3adant1 1121 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) = 0) → ({𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∪ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}) ∈ dom vol) |
166 | 165 | adantr 481 |
. . . 4
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) = 0) ∧ 𝑏 ∈ ran (,)) → ({𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∪ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}) ∈ dom vol) |
167 | 45, 166 | eqeltrd 2881 |
. . 3
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) = 0) ∧ 𝑏 ∈ ran (,)) → (◡𝐹 “ 𝑏) ∈ dom vol) |
168 | 167 | ralrimiva 3147 |
. 2
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) = 0) → ∀𝑏 ∈ ran (,)(◡𝐹 “ 𝑏) ∈ dom vol) |
169 | | ismbf 23900 |
. . 3
⊢ (𝐹:𝐴⟶ℝ → (𝐹 ∈ MblFn ↔ ∀𝑏 ∈ ran (,)(◡𝐹 “ 𝑏) ∈ dom vol)) |
170 | 169 | 3ad2ant1 1124 |
. 2
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) = 0) → (𝐹 ∈ MblFn ↔ ∀𝑏 ∈ ran (,)(◡𝐹 “ 𝑏) ∈ dom vol)) |
171 | 168, 170 | mpbird 258 |
1
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) = 0) → 𝐹 ∈ MblFn) |