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 --> RR /\ A e. dom vol /\ ( vol* ` ( A \ ( ( `' ( ( ( topGen ` ran (,) ) |`t A ) CnP ( topGen ` ran (,) ) ) o. _E ) " { F } ) ) ) = 0 ) -> F e. MblFn )

Proof

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