Metamath Proof Explorer

Theorem cnambfre

Description: A real-valued, a.e. continuous function is measurable. (Contributed by Brendan Leahy, 4-Apr-2018)

Ref Expression
Assertion cnambfre ⊢F:A⟶ℝ∧A∈dom⁡vol∧vol*⁡A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=0→F∈MblFn

Proof

Step Hyp Ref Expression
1 id ⊢F:A⟶ℝ→F:A⟶ℝ
2 1 feqmptd ⊢F:A⟶ℝ→F=x∈A⟼F⁡x
3 2 cnveqd ⊢F:A⟶ℝ→F-1=x∈A⟼F⁡x-1
4 3 imaeq1d ⊢F:A⟶ℝ→F-1b=x∈A⟼F⁡x-1b
5 4 ad2antrr ⊢F:A⟶ℝ∧A∈dom⁡vol∧b∈ran⁡.→F-1b=x∈A⟼F⁡x-1b
6 exmid ⊢F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∨¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x
7 6 biantrur ⊢F⁡x∈b↔F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∨¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b
8 andir ⊢F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∨¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b↔F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b∨¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b
9 7 8 bitri ⊢F⁡x∈b↔F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b∨¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b
10 retopbas ⊢ran⁡.∈TopBases
11 bastg ⊢ran⁡.∈TopBases→ran⁡.⊆topGen⁡ran⁡.
12 10 11 ax-mp ⊢ran⁡.⊆topGen⁡ran⁡.
13 12 sseli ⊢b∈ran⁡.→b∈topGen⁡ran⁡.
14 13 ad2antlr ⊢F:A⟶ℝ∧A∈dom⁡vol∧b∈ran⁡.∧x∈A→b∈topGen⁡ran⁡.
15 cnpimaex ⊢F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧b∈topGen⁡ran⁡.∧F⁡x∈b→∃y∈topGen⁡ran⁡.↾𝑡Ax∈y∧Fy⊆b
16 15 3com12 ⊢b∈topGen⁡ran⁡.∧F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b→∃y∈topGen⁡ran⁡.↾𝑡Ax∈y∧Fy⊆b
17 16 3expa ⊢b∈topGen⁡ran⁡.∧F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b→∃y∈topGen⁡ran⁡.↾𝑡Ax∈y∧Fy⊆b
18 14 17 sylanl1 ⊢F:A⟶ℝ∧A∈dom⁡vol∧b∈ran⁡.∧x∈A∧F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b→∃y∈topGen⁡ran⁡.↾𝑡Ax∈y∧Fy⊆b
19 18 ex ⊢F:A⟶ℝ∧A∈dom⁡vol∧b∈ran⁡.∧x∈A∧F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x→F⁡x∈b→∃y∈topGen⁡ran⁡.↾𝑡Ax∈y∧Fy⊆b
20 simprrr ⊢F:A⟶ℝ∧A∈dom⁡vol∧y∈topGen⁡ran⁡.↾𝑡A∧x∈y∧Fy⊆b→Fy⊆b
21 ffn ⊢F:A⟶ℝ→FFnA
22 21 adantr ⊢F:A⟶ℝ∧A∈dom⁡vol→FFnA
23 restsspw ⊢topGen⁡ran⁡.↾𝑡A⊆𝒫A
24 23 sseli ⊢y∈topGen⁡ran⁡.↾𝑡A→y∈𝒫A
25 24 elpwid ⊢y∈topGen⁡ran⁡.↾𝑡A→y⊆A
26 simpl ⊢x∈y∧Fy⊆b→x∈y
27 fnfvima ⊢FFnA∧y⊆A∧x∈y→F⁡x∈Fy
28 22 25 26 27 syl3an ⊢F:A⟶ℝ∧A∈dom⁡vol∧y∈topGen⁡ran⁡.↾𝑡A∧x∈y∧Fy⊆b→F⁡x∈Fy
29 28 3expb ⊢F:A⟶ℝ∧A∈dom⁡vol∧y∈topGen⁡ran⁡.↾𝑡A∧x∈y∧Fy⊆b→F⁡x∈Fy
30 20 29 sseldd ⊢F:A⟶ℝ∧A∈dom⁡vol∧y∈topGen⁡ran⁡.↾𝑡A∧x∈y∧Fy⊆b→F⁡x∈b
31 30 rexlimdvaa ⊢F:A⟶ℝ∧A∈dom⁡vol→∃y∈topGen⁡ran⁡.↾𝑡Ax∈y∧Fy⊆b→F⁡x∈b
32 31 ad3antrrr ⊢F:A⟶ℝ∧A∈dom⁡vol∧b∈ran⁡.∧x∈A∧F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x→∃y∈topGen⁡ran⁡.↾𝑡Ax∈y∧Fy⊆b→F⁡x∈b
33 19 32 impbid ⊢F:A⟶ℝ∧A∈dom⁡vol∧b∈ran⁡.∧x∈A∧F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x→F⁡x∈b↔∃y∈topGen⁡ran⁡.↾𝑡Ax∈y∧Fy⊆b
34 33 pm5.32da ⊢F:A⟶ℝ∧A∈dom⁡vol∧b∈ran⁡.∧x∈A→F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b↔F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧∃y∈topGen⁡ran⁡.↾𝑡Ax∈y∧Fy⊆b
35 r19.42v ⊢∃y∈topGen⁡ran⁡.↾𝑡AF∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b↔F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧∃y∈topGen⁡ran⁡.↾𝑡Ax∈y∧Fy⊆b
36 34 35 bitr4di ⊢F:A⟶ℝ∧A∈dom⁡vol∧b∈ran⁡.∧x∈A→F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b↔∃y∈topGen⁡ran⁡.↾𝑡AF∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b
37 36 orbi1d ⊢F:A⟶ℝ∧A∈dom⁡vol∧b∈ran⁡.∧x∈A→F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b∨¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b↔∃y∈topGen⁡ran⁡.↾𝑡AF∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b∨¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b
38 9 37 bitrid ⊢F:A⟶ℝ∧A∈dom⁡vol∧b∈ran⁡.∧x∈A→F⁡x∈b↔∃y∈topGen⁡ran⁡.↾𝑡AF∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b∨¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b
39 38 rabbidva ⊢F:A⟶ℝ∧A∈dom⁡vol∧b∈ran⁡.→x∈A|F⁡x∈b=x∈A|∃y∈topGen⁡ran⁡.↾𝑡AF∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b∨¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b
40 eqid ⊢x∈A⟼F⁡x=x∈A⟼F⁡x
41 40 mptpreima ⊢x∈A⟼F⁡x-1b=x∈A|F⁡x∈b
42 unrab ⊢x∈A|∃y∈topGen⁡ran⁡.↾𝑡AF∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b∪x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b=x∈A|∃y∈topGen⁡ran⁡.↾𝑡AF∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b∨¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b
43 39 41 42 3eqtr4g ⊢F:A⟶ℝ∧A∈dom⁡vol∧b∈ran⁡.→x∈A⟼F⁡x-1b=x∈A|∃y∈topGen⁡ran⁡.↾𝑡AF∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b∪x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b
44 5 43 eqtrd ⊢F:A⟶ℝ∧A∈dom⁡vol∧b∈ran⁡.→F-1b=x∈A|∃y∈topGen⁡ran⁡.↾𝑡AF∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b∪x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b
45 44 3adantl3 ⊢F:A⟶ℝ∧A∈dom⁡vol∧vol*⁡A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=0∧b∈ran⁡.→F-1b=x∈A|∃y∈topGen⁡ran⁡.↾𝑡AF∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b∪x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b
46 incom ⊢⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∩x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x=x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∩⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b
47 dfin4 ⊢⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∩x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x=⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x
48 inrab ⊢x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∩x∈A|x∈y∧Fy⊆b=x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b
49 48 a1i ⊢y∈topGen⁡ran⁡.↾𝑡A→x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∩x∈A|x∈y∧Fy⊆b=x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b
50 49 iuneq2i ⊢⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∩x∈A|x∈y∧Fy⊆b=⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b
51 iunin2 ⊢⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∩x∈A|x∈y∧Fy⊆b=x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∩⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b
52 iunrab ⊢⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b=x∈A|∃y∈topGen⁡ran⁡.↾𝑡AF∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b
53 50 51 52 3eqtr3i ⊢x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∩⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b=x∈A|∃y∈topGen⁡ran⁡.↾𝑡AF∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b
54 46 47 53 3eqtr3i ⊢⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x=x∈A|∃y∈topGen⁡ran⁡.↾𝑡AF∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b
55 eqeq2 ⊢y=ifFy⊆by∅→x∈A|x∈y∧Fy⊆b=y↔x∈A|x∈y∧Fy⊆b=ifFy⊆by∅
56 eqeq2 ⊢∅=ifFy⊆by∅→x∈A|x∈y∧Fy⊆b=∅↔x∈A|x∈y∧Fy⊆b=ifFy⊆by∅
57 simprrl ⊢y∈topGen⁡ran⁡.↾𝑡A∧Fy⊆b∧x∈A∧x∈y∧Fy⊆b→x∈y
58 25 adantr ⊢y∈topGen⁡ran⁡.↾𝑡A∧Fy⊆b→y⊆A
59 58 sselda ⊢y∈topGen⁡ran⁡.↾𝑡A∧Fy⊆b∧x∈y→x∈A
60 pm3.22 ⊢Fy⊆b∧x∈y→x∈y∧Fy⊆b
61 60 adantll ⊢y∈topGen⁡ran⁡.↾𝑡A∧Fy⊆b∧x∈y→x∈y∧Fy⊆b
62 59 61 jca ⊢y∈topGen⁡ran⁡.↾𝑡A∧Fy⊆b∧x∈y→x∈A∧x∈y∧Fy⊆b
63 57 62 impbida ⊢y∈topGen⁡ran⁡.↾𝑡A∧Fy⊆b→x∈A∧x∈y∧Fy⊆b↔x∈y
64 63 abbidv ⊢y∈topGen⁡ran⁡.↾𝑡A∧Fy⊆b→x|x∈A∧x∈y∧Fy⊆b=x|x∈y
65 df-rab ⊢x∈A|x∈y∧Fy⊆b=x|x∈A∧x∈y∧Fy⊆b
66 cvjust ⊢y=x|x∈y
67 64 65 66 3eqtr4g ⊢y∈topGen⁡ran⁡.↾𝑡A∧Fy⊆b→x∈A|x∈y∧Fy⊆b=y
68 simpr ⊢x∈y∧Fy⊆b→Fy⊆b
69 68 con3i ⊢¬Fy⊆b→¬x∈y∧Fy⊆b
70 69 ralrimivw ⊢¬Fy⊆b→∀x∈A¬x∈y∧Fy⊆b
71 rabeq0 ⊢x∈A|x∈y∧Fy⊆b=∅↔∀x∈A¬x∈y∧Fy⊆b
72 70 71 sylibr ⊢¬Fy⊆b→x∈A|x∈y∧Fy⊆b=∅
73 72 adantl ⊢y∈topGen⁡ran⁡.↾𝑡A∧¬Fy⊆b→x∈A|x∈y∧Fy⊆b=∅
74 55 56 67 73 ifbothda ⊢y∈topGen⁡ran⁡.↾𝑡A→x∈A|x∈y∧Fy⊆b=ifFy⊆by∅
75 74 iuneq2i ⊢⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b=⋃y∈topGen⁡ran⁡.↾𝑡AifFy⊆by∅
76 retop ⊢topGen⁡ran⁡.∈Top
77 resttop ⊢topGen⁡ran⁡.∈Top∧A∈dom⁡vol→topGen⁡ran⁡.↾𝑡A∈Top
78 76 77 mpan ⊢A∈dom⁡vol→topGen⁡ran⁡.↾𝑡A∈Top
79 0opn ⊢topGen⁡ran⁡.↾𝑡A∈Top→∅∈topGen⁡ran⁡.↾𝑡A
80 78 79 syl ⊢A∈dom⁡vol→∅∈topGen⁡ran⁡.↾𝑡A
81 ifcl ⊢y∈topGen⁡ran⁡.↾𝑡A∧∅∈topGen⁡ran⁡.↾𝑡A→ifFy⊆by∅∈topGen⁡ran⁡.↾𝑡A
82 81 ancoms ⊢∅∈topGen⁡ran⁡.↾𝑡A∧y∈topGen⁡ran⁡.↾𝑡A→ifFy⊆by∅∈topGen⁡ran⁡.↾𝑡A
83 80 82 sylan ⊢A∈dom⁡vol∧y∈topGen⁡ran⁡.↾𝑡A→ifFy⊆by∅∈topGen⁡ran⁡.↾𝑡A
84 83 ralrimiva ⊢A∈dom⁡vol→∀y∈topGen⁡ran⁡.↾𝑡AifFy⊆by∅∈topGen⁡ran⁡.↾𝑡A
85 iunopn ⊢topGen⁡ran⁡.↾𝑡A∈Top∧∀y∈topGen⁡ran⁡.↾𝑡AifFy⊆by∅∈topGen⁡ran⁡.↾𝑡A→⋃y∈topGen⁡ran⁡.↾𝑡AifFy⊆by∅∈topGen⁡ran⁡.↾𝑡A
86 78 84 85 syl2anc ⊢A∈dom⁡vol→⋃y∈topGen⁡ran⁡.↾𝑡AifFy⊆by∅∈topGen⁡ran⁡.↾𝑡A
87 eqid ⊢topGen⁡ran⁡.↾𝑡A=topGen⁡ran⁡.↾𝑡A
88 87 subopnmbl ⊢A∈dom⁡vol∧⋃y∈topGen⁡ran⁡.↾𝑡AifFy⊆by∅∈topGen⁡ran⁡.↾𝑡A→⋃y∈topGen⁡ran⁡.↾𝑡AifFy⊆by∅∈dom⁡vol
89 86 88 mpdan ⊢A∈dom⁡vol→⋃y∈topGen⁡ran⁡.↾𝑡AifFy⊆by∅∈dom⁡vol
90 75 89 eqeltrid ⊢A∈dom⁡vol→⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∈dom⁡vol
91 difss ⊢⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x⊆⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b
92 ssrab2 ⊢x∈A|x∈y∧Fy⊆b⊆A
93 92 rgenw ⊢∀y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b⊆A
94 iunss ⊢⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b⊆A↔∀y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b⊆A
95 93 94 mpbir ⊢⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b⊆A
96 91 95 sstri ⊢⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x⊆A
97 mblss ⊢A∈dom⁡vol→A⊆ℝ
98 96 97 sstrid ⊢A∈dom⁡vol→⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x⊆ℝ
99 ssdif ⊢⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b⊆A→⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x⊆A∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x
100 95 99 ax-mp ⊢⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x⊆A∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x
101 rele ⊢Rel⁡E
102 elrelimasn ⊢Rel⁡E→topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∈EF↔FEtopGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x
103 101 102 ax-mp ⊢topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∈EF↔FEtopGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x
104 fvex ⊢topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∈V
105 104 epeli ⊢FEtopGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x↔F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x
106 103 105 bitr2i ⊢F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x↔topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∈EF
107 106 anbi2i ⊢x∈A∧F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x↔x∈A∧topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∈EF
108 ovex ⊢ℝA∈V
109 108 rabex ⊢f∈ℝA|∀b∈topGen⁡ran⁡.f⁡x∈b→∃y∈topGen⁡ran⁡.↾𝑡Ax∈y∧fy⊆b∈V
110 eqid ⊢x∈A⟼f∈ℝA|∀b∈topGen⁡ran⁡.f⁡x∈b→∃y∈topGen⁡ran⁡.↾𝑡Ax∈y∧fy⊆b=x∈A⟼f∈ℝA|∀b∈topGen⁡ran⁡.f⁡x∈b→∃y∈topGen⁡ran⁡.↾𝑡Ax∈y∧fy⊆b
111 109 110 fnmpti ⊢x∈A⟼f∈ℝA|∀b∈topGen⁡ran⁡.f⁡x∈b→∃y∈topGen⁡ran⁡.↾𝑡Ax∈y∧fy⊆bFnA
112 retopon ⊢topGen⁡ran⁡.∈TopOn⁡ℝ
113 resttopon ⊢topGen⁡ran⁡.∈TopOn⁡ℝ∧A⊆ℝ→topGen⁡ran⁡.↾𝑡A∈TopOn⁡A
114 112 97 113 sylancr ⊢A∈dom⁡vol→topGen⁡ran⁡.↾𝑡A∈TopOn⁡A
115 cnpfval ⊢topGen⁡ran⁡.↾𝑡A∈TopOn⁡A∧topGen⁡ran⁡.∈TopOn⁡ℝ→topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.=x∈A⟼f∈ℝA|∀b∈topGen⁡ran⁡.f⁡x∈b→∃y∈topGen⁡ran⁡.↾𝑡Ax∈y∧fy⊆b
116 114 112 115 sylancl ⊢A∈dom⁡vol→topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.=x∈A⟼f∈ℝA|∀b∈topGen⁡ran⁡.f⁡x∈b→∃y∈topGen⁡ran⁡.↾𝑡Ax∈y∧fy⊆b
117 116 fneq1d ⊢A∈dom⁡vol→topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.FnA↔x∈A⟼f∈ℝA|∀b∈topGen⁡ran⁡.f⁡x∈b→∃y∈topGen⁡ran⁡.↾𝑡Ax∈y∧fy⊆bFnA
118 111 117 mpbiri ⊢A∈dom⁡vol→topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.FnA
119 elpreima ⊢topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.FnA→x∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1EF↔x∈A∧topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∈EF
120 118 119 syl ⊢A∈dom⁡vol→x∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1EF↔x∈A∧topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∈EF
121 107 120 bitr4id ⊢A∈dom⁡vol→x∈A∧F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x↔x∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1EF
122 121 abbidv ⊢A∈dom⁡vol→x|x∈A∧F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x=x|x∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1EF
123 df-rab ⊢x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x=x|x∈A∧F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x
124 imaco ⊢topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1EF
125 abid2 ⊢x|x∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1EF=topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1EF
126 124 125 eqtr4i ⊢topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=x|x∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1EF
127 122 123 126 3eqtr4g ⊢A∈dom⁡vol→x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x=topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF
128 127 difeq2d ⊢A∈dom⁡vol→A∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x=A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF
129 100 128 sseqtrid ⊢A∈dom⁡vol→⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x⊆A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF
130 difss ⊢A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF⊆A
131 130 97 sstrid ⊢A∈dom⁡vol→A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF⊆ℝ
132 129 131 jca ⊢A∈dom⁡vol→⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x⊆A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF∧A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF⊆ℝ
133 ovolssnul ⊢⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x⊆A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF∧A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF⊆ℝ∧vol*⁡A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=0→vol*⁡⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x=0
134 133 3expa ⊢⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x⊆A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF∧A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF⊆ℝ∧vol*⁡A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=0→vol*⁡⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x=0
135 132 134 sylan ⊢A∈dom⁡vol∧vol*⁡A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=0→vol*⁡⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x=0
136 nulmbl ⊢⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x⊆ℝ∧vol*⁡⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x=0→⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∈dom⁡vol
137 98 135 136 syl2an2r ⊢A∈dom⁡vol∧vol*⁡A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=0→⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∈dom⁡vol
138 difmbl ⊢⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∈dom⁡vol∧⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∈dom⁡vol→⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∈dom⁡vol
139 90 137 138 syl2an2r ⊢A∈dom⁡vol∧vol*⁡A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=0→⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖⋃y∈topGen⁡ran⁡.↾𝑡Ax∈A|x∈y∧Fy⊆b∖x∈A|F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∈dom⁡vol
140 54 139 eqeltrrid ⊢A∈dom⁡vol∧vol*⁡A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=0→x∈A|∃y∈topGen⁡ran⁡.↾𝑡AF∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b∈dom⁡vol
141 ssrab2 ⊢x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b⊆A
142 141 97 sstrid ⊢A∈dom⁡vol→x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b⊆ℝ
143 124 eleq2i ⊢x∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF↔x∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1EF
144 ibar ⊢x∈A→topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∈EF↔x∈A∧topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∈EF
145 106 144 bitr2id ⊢x∈A→x∈A∧topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∈EF↔F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x
146 120 145 sylan9bb ⊢A∈dom⁡vol∧x∈A→x∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1EF↔F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x
147 143 146 bitr2id ⊢A∈dom⁡vol∧x∈A→F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x↔x∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF
148 147 notbid ⊢A∈dom⁡vol∧x∈A→¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x↔¬x∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF
149 148 biimpd ⊢A∈dom⁡vol∧x∈A→¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x→¬x∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF
150 149 adantrd ⊢A∈dom⁡vol∧x∈A→¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b→¬x∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF
151 150 ss2rabdv ⊢A∈dom⁡vol→x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b⊆x∈A|¬x∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF
152 dfdif2 ⊢A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=x∈A|¬x∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF
153 151 152 sseqtrrdi ⊢A∈dom⁡vol→x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b⊆A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF
154 153 131 jca ⊢A∈dom⁡vol→x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b⊆A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF∧A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF⊆ℝ
155 ovolssnul ⊢x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b⊆A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF∧A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF⊆ℝ∧vol*⁡A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=0→vol*⁡x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b=0
156 155 3expa ⊢x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b⊆A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF∧A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF⊆ℝ∧vol*⁡A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=0→vol*⁡x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b=0
157 154 156 sylan ⊢A∈dom⁡vol∧vol*⁡A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=0→vol*⁡x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b=0
158 nulmbl ⊢x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b⊆ℝ∧vol*⁡x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b=0→x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b∈dom⁡vol
159 142 157 158 syl2an2r ⊢A∈dom⁡vol∧vol*⁡A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=0→x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b∈dom⁡vol
160 unmbl ⊢x∈A|∃y∈topGen⁡ran⁡.↾𝑡AF∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b∈dom⁡vol∧x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b∈dom⁡vol→x∈A|∃y∈topGen⁡ran⁡.↾𝑡AF∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b∪x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b∈dom⁡vol
161 140 159 160 syl2anc ⊢A∈dom⁡vol∧vol*⁡A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=0→x∈A|∃y∈topGen⁡ran⁡.↾𝑡AF∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b∪x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b∈dom⁡vol
162 161 3adant1 ⊢F:A⟶ℝ∧A∈dom⁡vol∧vol*⁡A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=0→x∈A|∃y∈topGen⁡ran⁡.↾𝑡AF∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b∪x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b∈dom⁡vol
163 162 adantr ⊢F:A⟶ℝ∧A∈dom⁡vol∧vol*⁡A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=0∧b∈ran⁡.→x∈A|∃y∈topGen⁡ran⁡.↾𝑡AF∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧x∈y∧Fy⊆b∪x∈A|¬F∈topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.⁡x∧F⁡x∈b∈dom⁡vol
164 45 163 eqeltrd ⊢F:A⟶ℝ∧A∈dom⁡vol∧vol*⁡A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=0∧b∈ran⁡.→F-1b∈dom⁡vol
165 164 ralrimiva ⊢F:A⟶ℝ∧A∈dom⁡vol∧vol*⁡A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=0→∀b∈ran⁡.F-1b∈dom⁡vol
166 ismbf ⊢F:A⟶ℝ→F∈MblFn↔∀b∈ran⁡.F-1b∈dom⁡vol
167 166 3ad2ant1 ⊢F:A⟶ℝ∧A∈dom⁡vol∧vol*⁡A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=0→F∈MblFn↔∀b∈ran⁡.F-1b∈dom⁡vol
168 165 167 mpbird ⊢F:A⟶ℝ∧A∈dom⁡vol∧vol*⁡A∖topGen⁡ran⁡.↾𝑡ACnPtopGen⁡ran⁡.-1∘EF=0→F∈MblFn