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 x φ
smffmpt.s φ S SAlg
smffmpt.b φ x A B V
smffmpt.m φ x A B SMblFn S
Assertion smffmpt φ x A B : A

Proof

Step Hyp Ref Expression
1 smffmpt.x x φ
2 smffmpt.s φ S SAlg
3 smffmpt.b φ x A B V
4 smffmpt.m φ x A B SMblFn S
5 eqid dom x A B = dom x A B
6 2 4 5 smff φ x A B : dom x A B
7 eqid x A B = x A B
8 1 7 3 dmmptdf φ dom x A B = A
9 8 eqcomd φ A = dom x A B
10 9 feq2d φ x A B : A x A B : dom x A B
11 6 10 mpbird φ x A B : A