| Step | Hyp | Ref
| Expression |
| 1 | | id 22 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶ℝ → 𝐹:𝐴⟶ℝ) |
| 2 | 1 | feqmptd 6977 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶ℝ → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
| 3 | 2 | cnveqd 5886 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶ℝ → ◡𝐹 = ◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
| 4 | 3 | imaeq1d 6077 |
. . . . . . 7
⊢ (𝐹:𝐴⟶ℝ → (◡𝐹 “ 𝑏) = (◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) “ 𝑏)) |
| 5 | 4 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) → (◡𝐹 “ 𝑏) = (◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) “ 𝑏)) |
| 6 | | exmid 895 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ ((((topGen‘ran
(,)) ↾t 𝐴)
CnP (topGen‘ran (,)))‘𝑥) ∨ ¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)) |
| 7 | 6 | biantrur 530 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) ∈ 𝑏 ↔ ((𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∨ ¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)) ∧ (𝐹‘𝑥) ∈ 𝑏)) |
| 8 | | andir 1011 |
. . . . . . . . . 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 275 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) ∈ 𝑏 ↔ ((𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏) ∨ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏))) |
| 10 | | retopbas 24781 |
. . . . . . . . . . . . . . . . . 18
⊢ ran (,)
∈ TopBases |
| 11 | | bastg 22973 |
. . . . . . . . . . . . . . . . . 18
⊢ (ran (,)
∈ TopBases → ran (,) ⊆ (topGen‘ran (,))) |
| 12 | 10, 11 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ran (,)
⊆ (topGen‘ran (,)) |
| 13 | 12 | sseli 3979 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ ran (,) → 𝑏 ∈ (topGen‘ran
(,))) |
| 14 | 13 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) → 𝑏 ∈ (topGen‘ran
(,))) |
| 15 | | cnpimaex 23264 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ ((((topGen‘ran
(,)) ↾t 𝐴)
CnP (topGen‘ran (,)))‘𝑥) ∧ 𝑏 ∈ (topGen‘ran (,)) ∧ (𝐹‘𝑥) ∈ 𝑏) → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) |
| 16 | 15 | 3com12 1124 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 ∈ (topGen‘ran (,))
∧ 𝐹 ∈
((((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏) → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) |
| 17 | 16 | 3expa 1119 |
. . . . . . . . . . . . . . 15
⊢ (((𝑏 ∈ (topGen‘ran (,))
∧ 𝐹 ∈
((((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,)))‘𝑥)) ∧ (𝐹‘𝑥) ∈ 𝑏) → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) |
| 18 | 14, 17 | sylanl1 680 |
. . . . . . . . . . . . . 14
⊢
((((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) ∧ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)) ∧ (𝐹‘𝑥) ∈ 𝑏) → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) |
| 19 | 18 | ex 412 |
. . . . . . . . . . . . 13
⊢
(((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) ∧ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)) → ((𝐹‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))) |
| 20 | | simprrr 782 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ (𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))) → (𝐹 “ 𝑦) ⊆ 𝑏) |
| 21 | | ffn 6736 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:𝐴⟶ℝ → 𝐹 Fn 𝐴) |
| 22 | 21 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → 𝐹 Fn 𝐴) |
| 23 | | restsspw 17476 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((topGen‘ran (,)) ↾t 𝐴) ⊆ 𝒫 𝐴 |
| 24 | 23 | sseli 3979 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
→ 𝑦 ∈ 𝒫
𝐴) |
| 25 | 24 | elpwid 4609 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
→ 𝑦 ⊆ 𝐴) |
| 26 | | simpl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏) → 𝑥 ∈ 𝑦) |
| 27 | | fnfvima 7253 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ 𝑥 ∈ 𝑦) → (𝐹‘𝑥) ∈ (𝐹 “ 𝑦)) |
| 28 | 22, 25, 26, 27 | syl3an 1161 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) → (𝐹‘𝑥) ∈ (𝐹 “ 𝑦)) |
| 29 | 28 | 3expb 1121 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ (𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))) → (𝐹‘𝑥) ∈ (𝐹 “ 𝑦)) |
| 30 | 20, 29 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ (𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))) → (𝐹‘𝑥) ∈ 𝑏) |
| 31 | 30 | rexlimdvaa 3156 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏) → (𝐹‘𝑥) ∈ 𝑏)) |
| 32 | 31 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢
(((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) ∧ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)) → (∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏) → (𝐹‘𝑥) ∈ 𝑏)) |
| 33 | 19, 32 | impbid 212 |
. . . . . . . . . . . 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 3191 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
((topGen‘ran (,)) ↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) ↔ (𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))) |
| 36 | 34, 35 | bitr4di 289 |
. . . . . . . . . 10
⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏) ↔ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)))) |
| 37 | 36 | orbi1d 917 |
. . . . . . . . 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 | bitrid 283 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) ∈ 𝑏 ↔ (∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) ∨ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)))) |
| 39 | 38 | rabbidva 3443 |
. . . . . . 7
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) → {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ 𝑏} = {𝑥 ∈ 𝐴 ∣ (∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) ∨ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏))}) |
| 40 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) |
| 41 | 40 | mptpreima 6258 |
. . . . . . 7
⊢ (◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) “ 𝑏) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ 𝑏} |
| 42 | | unrab 4315 |
. . . . . . 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 2802 |
. . . . . 6
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) → (◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) “ 𝑏) = ({𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∪ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)})) |
| 44 | 5, 43 | eqtrd 2777 |
. . . . 5
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑏 ∈ ran (,)) → (◡𝐹 “ 𝑏) = ({𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∪ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)})) |
| 45 | 44 | 3adantl3 1169 |
. . . 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 4209 |
. . . . . . . . 9
⊢ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∩ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) = ({𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)} ∩ ∪
𝑦 ∈ ((topGen‘ran
(,)) ↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)}) |
| 47 | | dfin4 4278 |
. . . . . . . . 9
⊢ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∩ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) = (∪
𝑦 ∈ ((topGen‘ran
(,)) ↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)})) |
| 48 | | inrab 4316 |
. . . . . . . . . . . 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 5013 |
. . . . . . . . . 10
⊢ ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)({𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)} ∩ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)}) = ∪
𝑦 ∈ ((topGen‘ran
(,)) ↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} |
| 51 | | iunin2 5071 |
. . . . . . . . . 10
⊢ ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)({𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)} ∩ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)}) = ({𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)} ∩ ∪
𝑦 ∈ ((topGen‘ran
(,)) ↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)}) |
| 52 | | iunrab 5052 |
. . . . . . . . . 10
⊢ ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} |
| 53 | 50, 51, 52 | 3eqtr3i 2773 |
. . . . . . . . 9
⊢ ({𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)} ∩ ∪
𝑦 ∈ ((topGen‘ran
(,)) ↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)}) = {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} |
| 54 | 46, 47, 53 | 3eqtr3i 2773 |
. . . . . . . 8
⊢ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)})) = {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} |
| 55 | | eqeq2 2749 |
. . . . . . . . . . . 12
⊢ (𝑦 = if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) → ({𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = 𝑦 ↔ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅))) |
| 56 | | eqeq2 2749 |
. . . . . . . . . . . 12
⊢ (∅
= if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) → ({𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = ∅ ↔ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅))) |
| 57 | | simprrl 781 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝐹 “ 𝑦) ⊆ 𝑏) ∧ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))) → 𝑥 ∈ 𝑦) |
| 58 | 25 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝐹 “ 𝑦) ⊆ 𝑏) → 𝑦 ⊆ 𝐴) |
| 59 | 58 | sselda 3983 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝐹 “ 𝑦) ⊆ 𝑏) ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴) |
| 60 | | pm3.22 459 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 “ 𝑦) ⊆ 𝑏 ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) |
| 61 | 60 | adantll 714 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝐹 “ 𝑦) ⊆ 𝑏) ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) |
| 62 | 59, 61 | jca 511 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝐹 “ 𝑦) ⊆ 𝑏) ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))) |
| 63 | 57, 62 | impbida 801 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝐹 “ 𝑦) ⊆ 𝑏) → ((𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) ↔ 𝑥 ∈ 𝑦)) |
| 64 | 63 | abbidv 2808 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝐹 “ 𝑦) ⊆ 𝑏) → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} = {𝑥 ∣ 𝑥 ∈ 𝑦}) |
| 65 | | df-rab 3437 |
. . . . . . . . . . . . 13
⊢ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} |
| 66 | | cvjust 2731 |
. . . . . . . . . . . . 13
⊢ 𝑦 = {𝑥 ∣ 𝑥 ∈ 𝑦} |
| 67 | 64, 65, 66 | 3eqtr4g 2802 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ (𝐹 “ 𝑦) ⊆ 𝑏) → {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = 𝑦) |
| 68 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏) → (𝐹 “ 𝑦) ⊆ 𝑏) |
| 69 | 68 | con3i 154 |
. . . . . . . . . . . . . . 15
⊢ (¬
(𝐹 “ 𝑦) ⊆ 𝑏 → ¬ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) |
| 70 | 69 | ralrimivw 3150 |
. . . . . . . . . . . . . 14
⊢ (¬
(𝐹 “ 𝑦) ⊆ 𝑏 → ∀𝑥 ∈ 𝐴 ¬ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) |
| 71 | | rabeq0 4388 |
. . . . . . . . . . . . . 14
⊢ ({𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)) |
| 72 | 70, 71 | sylibr 234 |
. . . . . . . . . . . . 13
⊢ (¬
(𝐹 “ 𝑦) ⊆ 𝑏 → {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = ∅) |
| 73 | 72 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ ¬ (𝐹 “
𝑦) ⊆ 𝑏) → {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = ∅) |
| 74 | 55, 56, 67, 73 | ifbothda 4564 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
→ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅)) |
| 75 | 74 | iuneq2i 5013 |
. . . . . . . . . 10
⊢ ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} = ∪
𝑦 ∈ ((topGen‘ran
(,)) ↾t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) |
| 76 | | retop 24782 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) ∈ Top |
| 77 | | resttop 23168 |
. . . . . . . . . . . . 13
⊢
(((topGen‘ran (,)) ∈ Top ∧ 𝐴 ∈ dom vol) → ((topGen‘ran
(,)) ↾t 𝐴)
∈ Top) |
| 78 | 76, 77 | mpan 690 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom vol →
((topGen‘ran (,)) ↾t 𝐴) ∈ Top) |
| 79 | | 0opn 22910 |
. . . . . . . . . . . . . . 15
⊢
(((topGen‘ran (,)) ↾t 𝐴) ∈ Top → ∅ ∈
((topGen‘ran (,)) ↾t 𝐴)) |
| 80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom vol → ∅
∈ ((topGen‘ran (,)) ↾t 𝐴)) |
| 81 | | ifcl 4571 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)
∧ ∅ ∈ ((topGen‘ran (,)) ↾t 𝐴)) → if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,))
↾t 𝐴)) |
| 82 | 81 | ancoms 458 |
. . . . . . . . . . . . . 14
⊢ ((∅
∈ ((topGen‘ran (,)) ↾t 𝐴) ∧ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴))
→ if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,))
↾t 𝐴)) |
| 83 | 80, 82 | sylan 580 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ dom vol ∧ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴))
→ if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,))
↾t 𝐴)) |
| 84 | 83 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom vol →
∀𝑦 ∈
((topGen‘ran (,)) ↾t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,))
↾t 𝐴)) |
| 85 | | iunopn 22904 |
. . . . . . . . . . . 12
⊢
((((topGen‘ran (,)) ↾t 𝐴) ∈ Top ∧ ∀𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,))
↾t 𝐴))
→ ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,))
↾t 𝐴)) |
| 86 | 78, 84, 85 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom vol → ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,))
↾t 𝐴)) |
| 87 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
((topGen‘ran (,)) ↾t 𝐴) = ((topGen‘ran (,))
↾t 𝐴) |
| 88 | 87 | subopnmbl 25639 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom vol ∧ ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ ((topGen‘ran (,))
↾t 𝐴))
→ ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ dom vol) |
| 89 | 86, 88 | mpdan 687 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom vol → ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)if((𝐹 “ 𝑦) ⊆ 𝑏, 𝑦, ∅) ∈ dom vol) |
| 90 | 75, 89 | eqeltrid 2845 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom vol → ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∈ dom vol) |
| 91 | | difss 4136 |
. . . . . . . . . . . 12
⊢ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ⊆ ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} |
| 92 | | ssrab2 4080 |
. . . . . . . . . . . . . 14
⊢ {𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ⊆ 𝐴 |
| 93 | 92 | rgenw 3065 |
. . . . . . . . . . . . 13
⊢
∀𝑦 ∈
((topGen‘ran (,)) ↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ⊆ 𝐴 |
| 94 | | iunss 5045 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ⊆ 𝐴 ↔ ∀𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ⊆ 𝐴) |
| 95 | 93, 94 | mpbir 231 |
. . . . . . . . . . . 12
⊢ ∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ⊆ 𝐴 |
| 96 | 91, 95 | sstri 3993 |
. . . . . . . . . . 11
⊢ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ⊆ 𝐴 |
| 97 | | mblss 25566 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
| 98 | 96, 97 | sstrid 3995 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom vol → (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ⊆ ℝ) |
| 99 | | ssdif 4144 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ⊆ 𝐴 → (∪
𝑦 ∈ ((topGen‘ran
(,)) ↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ⊆ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)})) |
| 100 | 95, 99 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ⊆ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) |
| 101 | | rele 5837 |
. . . . . . . . . . . . . . . . . . . 20
⊢ Rel
E |
| 102 | | elrelimasn 6104 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Rel E
→ (((((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹}) ↔ 𝐹 E ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥))) |
| 103 | 101, 102 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹}) ↔ 𝐹 E ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)) |
| 104 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,)))‘𝑥) ∈ V |
| 105 | 104 | epeli 5586 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 E ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ↔ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)) |
| 106 | 103, 105 | bitr2i 276 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ ((((topGen‘ran
(,)) ↾t 𝐴)
CnP (topGen‘ran (,)))‘𝑥) ↔ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹})) |
| 107 | 106 | anbi2i 623 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹}))) |
| 108 | | ovex 7464 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℝ
↑m 𝐴)
∈ V |
| 109 | 108 | rabex 5339 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑓 ∈ (ℝ
↑m 𝐴)
∣ ∀𝑏 ∈
(topGen‘ran (,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))} ∈ V |
| 110 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝐴 ↦ {𝑓 ∈ (ℝ ↑m 𝐴) ∣ ∀𝑏 ∈ (topGen‘ran
(,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))}) = (𝑥 ∈ 𝐴 ↦ {𝑓 ∈ (ℝ ↑m 𝐴) ∣ ∀𝑏 ∈ (topGen‘ran
(,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))}) |
| 111 | 109, 110 | fnmpti 6711 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐴 ↦ {𝑓 ∈ (ℝ ↑m 𝐴) ∣ ∀𝑏 ∈ (topGen‘ran
(,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))}) Fn 𝐴 |
| 112 | | retopon 24784 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
| 113 | | resttopon 23169 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ 𝐴 ⊆ ℝ) →
((topGen‘ran (,)) ↾t 𝐴) ∈ (TopOn‘𝐴)) |
| 114 | 112, 97, 113 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ dom vol →
((topGen‘ran (,)) ↾t 𝐴) ∈ (TopOn‘𝐴)) |
| 115 | | cnpfval 23242 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((topGen‘ran (,)) ↾t 𝐴) ∈ (TopOn‘𝐴) ∧ (topGen‘ran (,)) ∈
(TopOn‘ℝ)) → (((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) = (𝑥 ∈ 𝐴 ↦ {𝑓 ∈ (ℝ ↑m 𝐴) ∣ ∀𝑏 ∈ (topGen‘ran
(,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))})) |
| 116 | 114, 112,
115 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ dom vol →
(((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,))) = (𝑥 ∈ 𝐴 ↦ {𝑓 ∈ (ℝ ↑m 𝐴) ∣ ∀𝑏 ∈ (topGen‘ran
(,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))})) |
| 117 | 116 | fneq1d 6661 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ dom vol →
((((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,))) Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ {𝑓 ∈ (ℝ ↑m 𝐴) ∣ ∀𝑏 ∈ (topGen‘ran
(,))((𝑓‘𝑥) ∈ 𝑏 → ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝑥 ∈ 𝑦 ∧ (𝑓 “ 𝑦) ⊆ 𝑏))}) Fn 𝐴)) |
| 118 | 111, 117 | mpbiri 258 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ dom vol →
(((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,))) Fn 𝐴) |
| 119 | | elpreima 7078 |
. . . . . . . . . . . . . . . . . 18
⊢
((((topGen‘ran (,)) ↾t 𝐴) CnP (topGen‘ran (,))) Fn 𝐴 → (𝑥 ∈ (◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) “ ( E “ {𝐹})) ↔ (𝑥 ∈ 𝐴 ∧ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹})))) |
| 120 | 118, 119 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ dom vol → (𝑥 ∈ (◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) “ ( E “ {𝐹})) ↔ (𝑥 ∈ 𝐴 ∧ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹})))) |
| 121 | 107, 120 | bitr4id 290 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ dom vol → ((𝑥 ∈ 𝐴 ∧ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)) ↔ 𝑥 ∈ (◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) “ ( E “ {𝐹})))) |
| 122 | 121 | abbidv 2808 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom vol → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥))} = {𝑥 ∣ 𝑥 ∈ (◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) “ ( E “ {𝐹}))}) |
| 123 | | df-rab 3437 |
. . . . . . . . . . . . . . 15
⊢ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥))} |
| 124 | | imaco 6271 |
. . . . . . . . . . . . . . . 16
⊢ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}) = (◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) “ ( E “ {𝐹})) |
| 125 | | abid2 2879 |
. . . . . . . . . . . . . . . 16
⊢ {𝑥 ∣ 𝑥 ∈ (◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) “ ( E “ {𝐹}))} = (◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) “ ( E “ {𝐹})) |
| 126 | 124, 125 | eqtr4i 2768 |
. . . . . . . . . . . . . . 15
⊢ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}) = {𝑥 ∣ 𝑥 ∈ (◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) “ ( E “ {𝐹}))} |
| 127 | 122, 123,
126 | 3eqtr4g 2802 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom vol → {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)} = ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) |
| 128 | 127 | difeq2d 4126 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom vol → (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) = (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) |
| 129 | 100, 128 | sseqtrid 4026 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom vol → (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ⊆ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) |
| 130 | | difss 4136 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) ⊆ 𝐴 |
| 131 | 130, 97 | sstrid 3995 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom vol → (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) ⊆ ℝ) |
| 132 | 129, 131 | jca 511 |
. . . . . . . . . . 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 ) “ {𝐹})) ⊆ ℝ)) |
| 133 | | ovolssnul 25522 |
. . . . . . . . . . . 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) |
| 134 | 133 | 3expa 1119 |
. . . . . . . . . . 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) |
| 135 | 132, 134 | 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) |
| 136 | | nulmbl 25570 |
. . . . . . . . . 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) |
| 137 | 98, 135, 136 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom vol ∧
(vol*‘(𝐴 ∖
((◡(((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → (∪ 𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴){𝑥 ∈ 𝐴 ∣ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏)} ∖ {𝑥 ∈ 𝐴 ∣ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥)}) ∈ dom vol) |
| 138 | | difmbl 25578 |
. . . . . . . . 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) |
| 139 | 90, 137, 138 | syl2an2r 685 |
. . . . . . . 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) |
| 140 | 54, 139 | eqeltrrid 2846 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧
(vol*‘(𝐴 ∖
((◡(((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → {𝑥 ∈ 𝐴 ∣ ∃𝑦 ∈ ((topGen‘ran (,))
↾t 𝐴)(𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝑥 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑏))} ∈ dom vol) |
| 141 | | ssrab2 4080 |
. . . . . . . . 9
⊢ {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ 𝐴 |
| 142 | 141, 97 | sstrid 3995 |
. . . . . . . 8
⊢ (𝐴 ∈ dom vol → {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ ℝ) |
| 143 | 124 | eleq2i 2833 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}) ↔ 𝑥 ∈ (◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) “ ( E “ {𝐹}))) |
| 144 | | ibar 528 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝐴 → (((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹}) ↔ (𝑥 ∈ 𝐴 ∧ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹})))) |
| 145 | 106, 144 | bitr2id 284 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ∧ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∈ ( E “ {𝐹})) ↔ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥))) |
| 146 | 120, 145 | sylan9bb 509 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ (◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) “ ( E “ {𝐹})) ↔ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥))) |
| 147 | 143, 146 | bitr2id 284 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ∈ 𝐴) → (𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ↔ 𝑥 ∈ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) |
| 148 | 147 | notbid 318 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ∈ 𝐴) → (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ↔ ¬ 𝑥 ∈ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) |
| 149 | 148 | biimpd 229 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ∈ 𝐴) → (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) → ¬ 𝑥 ∈ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) |
| 150 | 149 | adantrd 491 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ∈ 𝐴) → ((¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏) → ¬ 𝑥 ∈ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) |
| 151 | 150 | ss2rabdv 4076 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom vol → {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})}) |
| 152 | | dfdif2 3960 |
. . . . . . . . . . 11
⊢ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})} |
| 153 | 151, 152 | sseqtrrdi 4025 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom vol → {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) |
| 154 | 153, 131 | jca 511 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom vol → ({𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) ∧ (𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹})) ⊆ ℝ)) |
| 155 | | ovolssnul 25522 |
. . . . . . . . . 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) |
| 156 | 155 | 3expa 1119 |
. . . . . . . . 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) |
| 157 | 154, 156 | sylan 580 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧
(vol*‘(𝐴 ∖
((◡(((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → (vol*‘{𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}) = 0) |
| 158 | | nulmbl 25570 |
. . . . . . . 8
⊢ (({𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ⊆ ℝ ∧ (vol*‘{𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)}) = 0) → {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ∈ dom vol) |
| 159 | 142, 157,
158 | syl2an2r 685 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧
(vol*‘(𝐴 ∖
((◡(((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,))) ∘ E ) “ {𝐹}))) = 0) → {𝑥 ∈ 𝐴 ∣ (¬ 𝐹 ∈ ((((topGen‘ran (,))
↾t 𝐴) CnP
(topGen‘ran (,)))‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝑏)} ∈ dom vol) |
| 160 | | unmbl 25572 |
. . . . . . 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) |
| 161 | 140, 159,
160 | 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) |
| 162 | 161 | 3adant1 1131 |
. . . . 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) |
| 163 | 162 | adantr 480 |
. . . 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) |
| 164 | 45, 163 | eqeltrd 2841 |
. . 3
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) = 0) ∧ 𝑏 ∈ ran (,)) → (◡𝐹 “ 𝑏) ∈ dom vol) |
| 165 | 164 | ralrimiva 3146 |
. 2
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) = 0) → ∀𝑏 ∈ ran (,)(◡𝐹 “ 𝑏) ∈ dom vol) |
| 166 | | ismbf 25663 |
. . 3
⊢ (𝐹:𝐴⟶ℝ → (𝐹 ∈ MblFn ↔ ∀𝑏 ∈ ran (,)(◡𝐹 “ 𝑏) ∈ dom vol)) |
| 167 | 166 | 3ad2ant1 1134 |
. 2
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) = 0) → (𝐹 ∈ MblFn ↔ ∀𝑏 ∈ ran (,)(◡𝐹 “ 𝑏) ∈ dom vol)) |
| 168 | 165, 167 | mpbird 257 |
1
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol ∧ (vol*‘(𝐴 ∖ ((◡(((topGen‘ran (,)) ↾t
𝐴) CnP (topGen‘ran
(,))) ∘ E ) “ {𝐹}))) = 0) → 𝐹 ∈ MblFn) |