Theorem smfid

Description: The identity function is Borel sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfid.j	⊢ 𝐽 = ( topGen ‘ ran (,) )
	smfid.b	⊢ 𝐵 = ( SalGen ‘ 𝐽 )
	smfid.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
Assertion	smfid	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ∈ ( SMblFn ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		smfid.j	⊢ 𝐽 = ( topGen ‘ ran (,) )
2		smfid.b	⊢ 𝐵 = ( SalGen ‘ 𝐽 )
3		smfid.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
4	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ ℝ )
5		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
6	4 5	sseldd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
7	6	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) : 𝐴 ⟶ ℝ )
8		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≤ 𝑧 ) → 𝑦 ≤ 𝑧 )
9		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑥 )
10	9	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) )
11		simpr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 = 𝑦 ) → 𝑥 = 𝑦 )
12		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
13	10 11 12 12	fvmptd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ‘ 𝑦 ) = 𝑦 )
14	13	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≤ 𝑧 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ‘ 𝑦 ) = 𝑦 )
15	9	a1i	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) )
16		simpr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑥 = 𝑧 ) → 𝑥 = 𝑧 )
17		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
18	15 16 17 17	fvmptd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ‘ 𝑧 ) = 𝑧 )
19	18	ad4ant13	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≤ 𝑧 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ‘ 𝑧 ) = 𝑧 )
20	14 19	breq12d	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≤ 𝑧 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ‘ 𝑧 ) ↔ 𝑦 ≤ 𝑧 ) )
21	8 20	mpbird	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≤ 𝑧 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ‘ 𝑧 ) )
22	21	ex	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 ≤ 𝑧 → ( ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ‘ 𝑧 ) ) )
23	22	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ‘ 𝑧 ) ) )
24	23	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ‘ 𝑧 ) ) )
25	3 7 24 1 2	incsmf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ∈ ( SMblFn ‘ 𝐵 ) )