preimaicomnf

Description: Preimage of an open interval, unbounded below. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	preimaicomnf.1	$⊢ φ \to F : A ⟶ ℝ^{*}$
	preimaicomnf.2	$⊢ φ \to B \in ℝ^{*}$
Assertion	preimaicomnf	$⊢ φ \to F^{-1} [[−∞, B)] = \{x \in A \| F (x) < B\}$

Proof

Step	Hyp	Ref	Expression
1		preimaicomnf.1	$⊢ φ \to F : A ⟶ ℝ^{*}$
2		preimaicomnf.2	$⊢ φ \to B \in ℝ^{*}$
3	1	ffnd	$⊢ φ \to F Fn A$
4		fncnvima2	$⊢ F Fn A \to F^{-1} [[−∞, B)] = \{x \in A \| F (x) \in [−∞, B)\}$
5	3 4	syl	$⊢ φ \to F^{-1} [[−∞, B)] = \{x \in A \| F (x) \in [−∞, B)\}$
6		mnfxr	$⊢ −∞ \in ℝ^{*}$
7	6	a1i	$⊢ ((φ \land x \in A) \land F (x) \in [−∞, B)) \to −∞ \in ℝ^{*}$
8	2	ad2antrr	$⊢ ((φ \land x \in A) \land F (x) \in [−∞, B)) \to B \in ℝ^{*}$
9		simpr	$⊢ ((φ \land x \in A) \land F (x) \in [−∞, B)) \to F (x) \in [−∞, B)$
10		icoltub	$⊢ (−∞ \in ℝ^{} \land B \in ℝ^{} \land F (x) \in [−∞, B)) \to F (x) < B$
11	7 8 9 10	syl3anc	$⊢ ((φ \land x \in A) \land F (x) \in [−∞, B)) \to F (x) < B$
12	11	ex	$⊢ (φ \land x \in A) \to (F (x) \in [−∞, B) \to F (x) < B)$
13	6	a1i	$⊢ ((φ \land x \in A) \land F (x) < B) \to −∞ \in ℝ^{*}$
14	2	ad2antrr	$⊢ ((φ \land x \in A) \land F (x) < B) \to B \in ℝ^{*}$
15	1	ffvelcdmda	$⊢ (φ \land x \in A) \to F (x) \in ℝ^{*}$
16	15	adantr	$⊢ ((φ \land x \in A) \land F (x) < B) \to F (x) \in ℝ^{*}$
17	15	mnfled	$⊢ (φ \land x \in A) \to −∞ \leq F (x)$
18	17	adantr	$⊢ ((φ \land x \in A) \land F (x) < B) \to −∞ \leq F (x)$
19		simpr	$⊢ ((φ \land x \in A) \land F (x) < B) \to F (x) < B$
20	13 14 16 18 19	elicod	$⊢ ((φ \land x \in A) \land F (x) < B) \to F (x) \in [−∞, B)$
21	20	ex	$⊢ (φ \land x \in A) \to (F (x) < B \to F (x) \in [−∞, B))$
22	12 21	impbid	$⊢ (φ \land x \in A) \to (F (x) \in [−∞, B) \leftrightarrow F (x) < B)$
23	22	rabbidva	$⊢ φ \to \{x \in A \| F (x) \in [−∞, B)\} = \{x \in A \| F (x) < B\}$
24	5 23	eqtrd	$⊢ φ \to F^{-1} [[−∞, B)] = \{x \in A \| F (x) < B\}$

Metamath Proof Explorer

Theorem preimaicomnf

Proof