i1fima

Description: Any preimage of a simple function is measurable. (Contributed by Mario Carneiro, 26-Jun-2014)

		Ref	Expression
	Assertion	i1fima	$⊢ F \in dom \int^{1} \to F^{-1} [A] \in dom vol$

Proof

Step	Hyp	Ref	Expression
1		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
2		ffun	$⊢ F : ℝ ⟶ ℝ \to Fun F$
3		inpreima	$⊢ Fun F \to F^{-1} [A \cap ran F] = F^{-1} [A] \cap F^{-1} [ran F]$
4		iunid	$⊢ ⋃_{y \in A \cap ran F} \{y\} = A \cap ran F$
5	4	imaeq2i	$⊢ F^{-1} [⋃_{y \in A \cap ran F} \{y\}] = F^{-1} [A \cap ran F]$
6		imaiun	$⊢ F^{-1} [⋃_{y \in A \cap ran F} \{y\}] = ⋃_{y \in A \cap ran F} F^{-1} [\{y\}]$
7	5 6	eqtr3i	$⊢ F^{-1} [A \cap ran F] = ⋃_{y \in A \cap ran F} F^{-1} [\{y\}]$
8		cnvimass	$⊢ F^{-1} [A] \subseteq dom F$
9		cnvimarndm	$⊢ F^{-1} [ran F] = dom F$
10	8 9	sseqtrri	$⊢ F^{-1} [A] \subseteq F^{-1} [ran F]$
11		df-ss	$⊢ F^{-1} [A] \subseteq F^{-1} [ran F] \leftrightarrow F^{-1} [A] \cap F^{-1} [ran F] = F^{-1} [A]$
12	10 11	mpbi	$⊢ F^{-1} [A] \cap F^{-1} [ran F] = F^{-1} [A]$
13	3 7 12	3eqtr3g	$⊢ Fun F \to ⋃_{y \in A \cap ran F} F^{-1} [\{y\}] = F^{-1} [A]$
14	1 2 13	3syl	$⊢ F \in dom \int^{1} \to ⋃_{y \in A \cap ran F} F^{-1} [\{y\}] = F^{-1} [A]$
15		i1frn	$⊢ F \in dom \int^{1} \to ran F \in Fin$
16		inss2	$⊢ A \cap ran F \subseteq ran F$
17		ssfi	$⊢ (ran F \in Fin \land A \cap ran F \subseteq ran F) \to A \cap ran F \in Fin$
18	15 16 17	sylancl	$⊢ F \in dom \int^{1} \to A \cap ran F \in Fin$
19		i1fmbf	$⊢ F \in dom \int^{1} \to F \in MblFn$
20	19	adantr	$⊢ (F \in dom \int^{1} \land y \in (A \cap ran F)) \to F \in MblFn$
21	1	adantr	$⊢ (F \in dom \int^{1} \land y \in (A \cap ran F)) \to F : ℝ ⟶ ℝ$
22	1	frnd	$⊢ F \in dom \int^{1} \to ran F \subseteq ℝ$
23	16 22	sstrid	$⊢ F \in dom \int^{1} \to A \cap ran F \subseteq ℝ$
24	23	sselda	$⊢ (F \in dom \int^{1} \land y \in (A \cap ran F)) \to y \in ℝ$
25		mbfimasn	$⊢ (F \in MblFn \land F : ℝ ⟶ ℝ \land y \in ℝ) \to F^{-1} [\{y\}] \in dom vol$
26	20 21 24 25	syl3anc	$⊢ (F \in dom \int^{1} \land y \in (A \cap ran F)) \to F^{-1} [\{y\}] \in dom vol$
27	26	ralrimiva	$⊢ F \in dom \int^{1} \to \forall y \in (A \cap ran F) F^{-1} [\{y\}] \in dom vol$
28		finiunmbl	$⊢ (A \cap ran F \in Fin \land \forall y \in (A \cap ran F) F^{-1} [\{y\}] \in dom vol) \to ⋃_{y \in A \cap ran F} F^{-1} [\{y\}] \in dom vol$
29	18 27 28	syl2anc	$⊢ F \in dom \int^{1} \to ⋃_{y \in A \cap ran F} F^{-1} [\{y\}] \in dom vol$
30	14 29	eqeltrrd	$⊢ F \in dom \int^{1} \to F^{-1} [A] \in dom vol$

Metamath Proof Explorer

Theorem i1fima

Proof