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 ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ∧ ( vol* ‘ ( 𝐴 ∖ ( ( ◡ ( ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) CnP ( topGen ‘ ran (,) ) ) ∘ E ) “ { 𝐹 } ) ) ) = 0 ) → 𝐹 ∈ MblFn )

Proof

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