Metamath Proof Explorer


Theorem smffmpt

Description: A function measurable w.r.t. to a sigma-algebra, is actually a function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smffmpt.x
|- F/ x ph
smffmpt.s
|- ( ph -> S e. SAlg )
smffmpt.b
|- ( ( ph /\ x e. A ) -> B e. V )
smffmpt.m
|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
Assertion smffmpt
|- ( ph -> ( x e. A |-> B ) : A --> RR )

Proof

Step Hyp Ref Expression
1 smffmpt.x
 |-  F/ x ph
2 smffmpt.s
 |-  ( ph -> S e. SAlg )
3 smffmpt.b
 |-  ( ( ph /\ x e. A ) -> B e. V )
4 smffmpt.m
 |-  ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
5 eqid
 |-  dom ( x e. A |-> B ) = dom ( x e. A |-> B )
6 2 4 5 smff
 |-  ( ph -> ( x e. A |-> B ) : dom ( x e. A |-> B ) --> RR )
7 eqid
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
8 1 7 3 dmmptdf
 |-  ( ph -> dom ( x e. A |-> B ) = A )
9 8 eqcomd
 |-  ( ph -> A = dom ( x e. A |-> B ) )
10 9 feq2d
 |-  ( ph -> ( ( x e. A |-> B ) : A --> RR <-> ( x e. A |-> B ) : dom ( x e. A |-> B ) --> RR ) )
11 6 10 mpbird
 |-  ( ph -> ( x e. A |-> B ) : A --> RR )