Metamath Proof Explorer


Theorem smf2id

Description: Twice the identity function is Borel sigma-measurable (just an example, to test previous general theorems). (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smf2id.j
|- J = ( topGen ` ran (,) )
smf2id.b
|- B = ( SalGen ` J )
smf2id.a
|- ( ph -> A C_ RR )
Assertion smf2id
|- ( ph -> ( x e. A |-> ( 2 x. x ) ) e. ( SMblFn ` B ) )

Proof

Step Hyp Ref Expression
1 smf2id.j
 |-  J = ( topGen ` ran (,) )
2 smf2id.b
 |-  B = ( SalGen ` J )
3 smf2id.a
 |-  ( ph -> A C_ RR )
4 nfv
 |-  F/ x ph
5 retop
 |-  ( topGen ` ran (,) ) e. Top
6 1 5 eqeltri
 |-  J e. Top
7 6 a1i
 |-  ( ph -> J e. Top )
8 7 2 salgencld
 |-  ( ph -> B e. SAlg )
9 reex
 |-  RR e. _V
10 9 a1i
 |-  ( ph -> RR e. _V )
11 10 3 ssexd
 |-  ( ph -> A e. _V )
12 3 adantr
 |-  ( ( ph /\ x e. A ) -> A C_ RR )
13 simpr
 |-  ( ( ph /\ x e. A ) -> x e. A )
14 12 13 sseldd
 |-  ( ( ph /\ x e. A ) -> x e. RR )
15 2re
 |-  2 e. RR
16 15 a1i
 |-  ( ph -> 2 e. RR )
17 1 2 3 smfid
 |-  ( ph -> ( x e. A |-> x ) e. ( SMblFn ` B ) )
18 4 8 11 14 16 17 smfmulc1
 |-  ( ph -> ( x e. A |-> ( 2 x. x ) ) e. ( SMblFn ` B ) )