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 ) )