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	$⊢ φ \to A \subseteq ℝ$
Assertion	smfid	$⊢ φ \to (x \in A ⟼ x) \in SMblFn (B)$

Proof

Step	Hyp	Ref	Expression
1		smfid.j	$⊢ J = topGen (ran (.))$
2		smfid.b	$⊢ B = SalGen (J)$
3		smfid.a	$⊢ φ \to A \subseteq ℝ$
4	3	adantr	$⊢ (φ \land x \in A) \to A \subseteq ℝ$
5		simpr	$⊢ (φ \land x \in A) \to x \in A$
6	4 5	sseldd	$⊢ (φ \land x \in A) \to x \in ℝ$
7	6	fmpttd	$⊢ φ \to (x \in A ⟼ x) : A ⟶ ℝ$
8		simpr	$⊢ (((φ \land y \in A) \land z \in A) \land y \leq z) \to y \leq z$
9		eqid	$⊢ (x \in A ⟼ x) = (x \in A ⟼ x)$
10	9	a1i	$⊢ (φ \land y \in A) \to (x \in A ⟼ x) = (x \in A ⟼ x)$
11		simpr	$⊢ ((φ \land y \in A) \land x = y) \to x = y$
12		simpr	$⊢ (φ \land y \in A) \to y \in A$
13	10 11 12 12	fvmptd	$⊢ (φ \land y \in A) \to (x \in A ⟼ x) (y) = y$
14	13	ad2antrr	$⊢ (((φ \land y \in A) \land z \in A) \land y \leq z) \to (x \in A ⟼ x) (y) = y$
15	9	a1i	$⊢ (φ \land z \in A) \to (x \in A ⟼ x) = (x \in A ⟼ x)$
16		simpr	$⊢ ((φ \land z \in A) \land x = z) \to x = z$
17		simpr	$⊢ (φ \land z \in A) \to z \in A$
18	15 16 17 17	fvmptd	$⊢ (φ \land z \in A) \to (x \in A ⟼ x) (z) = z$
19	18	ad4ant13	$⊢ (((φ \land y \in A) \land z \in A) \land y \leq z) \to (x \in A ⟼ x) (z) = z$
20	14 19	breq12d	$⊢ (((φ \land y \in A) \land z \in A) \land y \leq z) \to ((x \in A ⟼ x) (y) \leq (x \in A ⟼ x) (z) \leftrightarrow y \leq z)$
21	8 20	mpbird	$⊢ (((φ \land y \in A) \land z \in A) \land y \leq z) \to (x \in A ⟼ x) (y) \leq (x \in A ⟼ x) (z)$
22	21	ex	$⊢ ((φ \land y \in A) \land z \in A) \to (y \leq z \to (x \in A ⟼ x) (y) \leq (x \in A ⟼ x) (z))$
23	22	ralrimiva	$⊢ (φ \land y \in A) \to \forall z \in A (y \leq z \to (x \in A ⟼ x) (y) \leq (x \in A ⟼ x) (z))$
24	23	ralrimiva	$⊢ φ \to \forall y \in A \forall z \in A (y \leq z \to (x \in A ⟼ x) (y) \leq (x \in A ⟼ x) (z))$
25	3 7 24 1 2	incsmf	$⊢ φ \to (x \in A ⟼ x) \in SMblFn (B)$

Metamath Proof Explorer

Theorem smfid

Proof