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=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	smf2id.b	$$⊢B=\mathrm{SalGen}\left(J\right)$$
	smf2id.a	$$⊢\phi \to A\subseteq ℝ$$
Assertion	smf2id	$$⊢\phi \to \left(x\in A⟼2x\right)\in \mathrm{SMblFn}\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		smf2id.j	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
2		smf2id.b	$$⊢B=\mathrm{SalGen}\left(J\right)$$
3		smf2id.a	$$⊢\phi \to A\subseteq ℝ$$
4		nfv	$$⊢Ⅎx\phi$$
5		retop	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$$
6	1 5	eqeltri	$$⊢J\in \mathrm{Top}$$
7	6	a1i	$$⊢\phi \to J\in \mathrm{Top}$$
8	7 2	salgencld	$$⊢\phi \to B\in \mathrm{SAlg}$$
9		reex	$$⊢ℝ\in \mathrm{V}$$
10	9	a1i	$$⊢\phi \to ℝ\in \mathrm{V}$$
11	10 3	ssexd	$$⊢\phi \to A\in \mathrm{V}$$
12	3	adantr	$$⊢\left(\phi \wedge x\in A\right)\to A\subseteq ℝ$$
13		simpr	$$⊢\left(\phi \wedge x\in A\right)\to x\in A$$
14	12 13	sseldd	$$⊢\left(\phi \wedge x\in A\right)\to x\in ℝ$$
15		2re	$$⊢2\in ℝ$$
16	15	a1i	$$⊢\phi \to 2\in ℝ$$
17	1 2 3	smfid	$$⊢\phi \to \left(x\in A⟼x\right)\in \mathrm{SMblFn}\left(B\right)$$
18	4 8 11 14 16 17	smfmulc1	$$⊢\phi \to \left(x\in A⟼2x\right)\in \mathrm{SMblFn}\left(B\right)$$