Metamath Proof Explorer

Theorem smfid

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

Ref Expression
Hypotheses smfid.j ⊢ J = topGen ⁡ ran ⁡ .
smfid.b ⊢ B = SalGen ⁡ J
smfid.a ⊢ φ → A ⊆ ℝ
Assertion smfid ⊢ φ → x ∈ A ⟼ x ∈ SMblFn ⁡ B

Proof

Step Hyp Ref Expression
1 smfid.j ⊢ J = topGen ⁡ ran ⁡ .
2 smfid.b ⊢ B = SalGen ⁡ J
3 smfid.a ⊢ φ → A ⊆ ℝ
4 3 adantr ⊢ φ ∧ x ∈ A → A ⊆ ℝ
5 simpr ⊢ φ ∧ x ∈ A → x ∈ A
6 4 5 sseldd ⊢ φ ∧ x ∈ A → x ∈ ℝ
7 6 fmpttd ⊢ φ → x ∈ A ⟼ x : A ⟶ ℝ
8 simpr ⊢ φ ∧ y ∈ A ∧ z ∈ A ∧ y ≤ z → y ≤ z
9 eqid ⊢ x ∈ A ⟼ x = x ∈ A ⟼ x
10 9 a1i ⊢ φ ∧ y ∈ A → x ∈ A ⟼ x = x ∈ A ⟼ x
11 simpr ⊢ φ ∧ y ∈ A ∧ x = y → x = y
12 simpr ⊢ φ ∧ y ∈ A → y ∈ A
13 10 11 12 12 fvmptd ⊢ φ ∧ y ∈ A → x ∈ A ⟼ x ⁡ y = y
14 13 ad2antrr ⊢ φ ∧ y ∈ A ∧ z ∈ A ∧ y ≤ z → x ∈ A ⟼ x ⁡ y = y
15 9 a1i ⊢ φ ∧ z ∈ A → x ∈ A ⟼ x = x ∈ A ⟼ x
16 simpr ⊢ φ ∧ z ∈ A ∧ x = z → x = z
17 simpr ⊢ φ ∧ z ∈ A → z ∈ A
18 15 16 17 17 fvmptd ⊢ φ ∧ z ∈ A → x ∈ A ⟼ x ⁡ z = z
19 18 ad4ant13 ⊢ φ ∧ y ∈ A ∧ z ∈ A ∧ y ≤ z → x ∈ A ⟼ x ⁡ z = z
20 14 19 breq12d ⊢ φ ∧ y ∈ A ∧ z ∈ A ∧ y ≤ z → x ∈ A ⟼ x ⁡ y ≤ x ∈ A ⟼ x ⁡ z ↔ y ≤ z
21 8 20 mpbird ⊢ φ ∧ y ∈ A ∧ z ∈ A ∧ y ≤ z → x ∈ A ⟼ x ⁡ y ≤ x ∈ A ⟼ x ⁡ z
22 21 ex ⊢ φ ∧ y ∈ A ∧ z ∈ A → y ≤ z → x ∈ A ⟼ x ⁡ y ≤ x ∈ A ⟼ x ⁡ z
23 22 ralrimiva ⊢ φ ∧ y ∈ A → ∀ z ∈ A y ≤ z → x ∈ A ⟼ x ⁡ y ≤ x ∈ A ⟼ x ⁡ z
24 23 ralrimiva ⊢ φ → ∀ y ∈ A ∀ z ∈ A y ≤ z → x ∈ A ⟼ x ⁡ y ≤ x ∈ A ⟼ x ⁡ z
25 3 7 24 1 2 incsmf ⊢ φ → x ∈ A ⟼ x ∈ SMblFn ⁡ B