This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem i1fima2sn

Description: Preimage of a singleton. (Contributed by Mario Carneiro, 26-Jun-2014)

		Ref	Expression
	Assertion	i1fima2sn	$⊢ (F \in dom \int^{1} \land A \in (B ∖ \{0\})) \to vol (F^{-1} [\{A\}]) \in ℝ$

Step	Hyp	Ref	Expression
1		eldifn	$⊢ A \in (B ∖ \{0\}) \to \neg A \in \{0\}$
2		elsni	$⊢ 0 \in \{A\} \to 0 = A$
3		snidg	$⊢ 0 \in \{A\} \to 0 \in \{0\}$
4	2 3	eqeltrrd	$⊢ 0 \in \{A\} \to A \in \{0\}$
5	1 4	nsyl	$⊢ A \in (B ∖ \{0\}) \to \neg 0 \in \{A\}$
6		i1fima2	$⊢ (F \in dom \int^{1} \land \neg 0 \in \{A\}) \to vol (F^{-1} [\{A\}]) \in ℝ$
7	5 6	sylan2	$⊢ (F \in dom \int^{1} \land A \in (B ∖ \{0\})) \to vol (F^{-1} [\{A\}]) \in ℝ$