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 φ A
Assertion smf2id φ x A 2 x SMblFn B

Proof

Step Hyp Ref Expression
1 smf2id.j J = topGen ran .
2 smf2id.b B = SalGen J
3 smf2id.a φ A
4 nfv x φ
5 retop topGen ran . Top
6 1 5 eqeltri J Top
7 6 a1i φ J Top
8 7 2 salgencld φ B SAlg
9 reex V
10 9 a1i φ V
11 10 3 ssexd φ A V
12 3 adantr φ x A A
13 simpr φ x A x A
14 12 13 sseldd φ x A x
15 2re 2
16 15 a1i φ 2
17 1 2 3 smfid φ x A x SMblFn B
18 4 8 11 14 16 17 smfmulc1 φ x A 2 x SMblFn B