Metamath Proof Explorer

Theorem smfpimbor1lem2

Description: Given a sigma-measurable function, the preimage of a Borel set belongs to the subspace sigma-algebra induced by the domain of the function. Proposition 121E (f) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfpimbor1lem2.s 
|- ( ph -> S e. SAlg )
smfpimbor1lem2.f 
|- ( ph -> F e. ( SMblFn ` S ) )
smfpimbor1lem2.a 
|- D = dom F
smfpimbor1lem2.j 
|- J = ( topGen ` ran (,) )
smfpimbor1lem2.b 
|- B = ( SalGen ` J )
smfpimbor1lem2.e 
|- ( ph -> E e. B )
smfpimbor1lem2.p 
|- P = ( `' F " E )
smfpimbor1lem2.t 
|- T = { e e. ~P RR | ( `' F " e ) e. ( S |`t D ) }
Assertion smfpimbor1lem2 
|- ( ph -> P e. ( S |`t D ) )

Proof

Step Hyp Ref Expression
1 smfpimbor1lem2.s 
 |-  ( ph -> S e. SAlg )
2 smfpimbor1lem2.f 
 |-  ( ph -> F e. ( SMblFn ` S ) )
3 smfpimbor1lem2.a 
 |-  D = dom F
4 smfpimbor1lem2.j 
 |-  J = ( topGen ` ran (,) )
5 smfpimbor1lem2.b 
 |-  B = ( SalGen ` J )
6 smfpimbor1lem2.e 
 |-  ( ph -> E e. B )
7 smfpimbor1lem2.p 
 |-  P = ( `' F " E )
8 smfpimbor1lem2.t 
 |-  T = { e e. ~P RR | ( `' F " e ) e. ( S |`t D ) }
9 retop 
 |-  ( topGen ` ran (,) ) e. Top
10 4 9 eqeltri 
 |-  J e. Top
11 10 a1i 
 |-  ( ph -> J e. Top )
12 1 2 3 8 smfresal 
 |-  ( ph -> T e. SAlg )
13 1 adantr 
 |-  ( ( ph /\ x e. J ) -> S e. SAlg )
14 2 adantr 
 |-  ( ( ph /\ x e. J ) -> F e. ( SMblFn ` S ) )
15 simpr 
 |-  ( ( ph /\ x e. J ) -> x e. J )
16 13 14 3 4 15 8 smfpimbor1lem1 
 |-  ( ( ph /\ x e. J ) -> x e. T )
17 16 ssd 
 |-  ( ph -> J C_ T )
18 nfcv 
 |-  F/_ e x
19 nfrab1 
 |-  F/_ e { e e. ~P RR | ( `' F " e ) e. ( S |`t D ) }
20 8 19 nfcxfr 
 |-  F/_ e T
21 18 20 eluni2f 
 |-  ( x e. U. T <-> E. e e. T x e. e )
22 21 biimpi 
 |-  ( x e. U. T -> E. e e. T x e. e )
23 20 nfuni 
 |-  F/_ e U. T
24 18 23 nfel 
 |-  F/ e x e. U. T
25 nfv 
 |-  F/ e x e. RR
26 8 eleq2i 
 |-  ( e e. T <-> e e. { e e. ~P RR | ( `' F " e ) e. ( S |`t D ) } )
27 26 biimpi 
 |-  ( e e. T -> e e. { e e. ~P RR | ( `' F " e ) e. ( S |`t D ) } )
28 rabidim1 
 |-  ( e e. { e e. ~P RR | ( `' F " e ) e. ( S |`t D ) } -> e e. ~P RR )
29 27 28 syl 
 |-  ( e e. T -> e e. ~P RR )
30 elpwi 
 |-  ( e e. ~P RR -> e C_ RR )
31 29 30 syl 
 |-  ( e e. T -> e C_ RR )
32 31 adantr 
 |-  ( ( e e. T /\ x e. e ) -> e C_ RR )
33 simpr 
 |-  ( ( e e. T /\ x e. e ) -> x e. e )
34 32 33 sseldd 
 |-  ( ( e e. T /\ x e. e ) -> x e. RR )
35 34 ex 
 |-  ( e e. T -> ( x e. e -> x e. RR ) )
36 35 a1i 
 |-  ( x e. U. T -> ( e e. T -> ( x e. e -> x e. RR ) ) )
37 24 25 36 rexlimd 
 |-  ( x e. U. T -> ( E. e e. T x e. e -> x e. RR ) )
38 22 37 mpd 
 |-  ( x e. U. T -> x e. RR )
39 38 rgen 
 |-  A. x e. U. T x e. RR
40 dfss3 
 |-  ( U. T C_ RR <-> A. x e. U. T x e. RR )
41 39 40 mpbir 
 |-  U. T C_ RR
42 41 a1i 
 |-  ( ph -> U. T C_ RR )
43 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
44 4 eqcomi 
 |-  ( topGen ` ran (,) ) = J
45 44 unieqi 
 |-  U. ( topGen ` ran (,) ) = U. J
46 43 45 eqtr2i 
 |-  U. J = RR
47 46 a1i 
 |-  ( ph -> U. J = RR )
48 47 eqcomd 
 |-  ( ph -> RR = U. J )
49 17 unissd 
 |-  ( ph -> U. J C_ U. T )
50 48 49 eqsstrd 
 |-  ( ph -> RR C_ U. T )
51 42 50 eqssd 
 |-  ( ph -> U. T = RR )
52 51 47 eqtr4d 
 |-  ( ph -> U. T = U. J )
53 11 5 12 17 52 salgenss 
 |-  ( ph -> B C_ T )
54 53 6 sseldd 
 |-  ( ph -> E e. T )
55 imaeq2 
 |-  ( e = E -> ( `' F " e ) = ( `' F " E ) )
56 55 eleq1d 
 |-  ( e = E -> ( ( `' F " e ) e. ( S |`t D ) <-> ( `' F " E ) e. ( S |`t D ) ) )
57 56 8 elrab2 
 |-  ( E e. T <-> ( E e. ~P RR /\ ( `' F " E ) e. ( S |`t D ) ) )
58 54 57 sylib 
 |-  ( ph -> ( E e. ~P RR /\ ( `' F " E ) e. ( S |`t D ) ) )
59 58 simprd 
 |-  ( ph -> ( `' F " E ) e. ( S |`t D ) )
60 7 59 eqeltrid 
 |-  ( ph -> P e. ( S |`t D ) )