Theorem pimltmnf2

Description: Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound -oo , is the empty set. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	pimltmnf2.1	⊢ Ⅎ 𝑥 𝐹
	pimltmnf2.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
Assertion	pimltmnf2	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < -∞ } = ∅ )

Proof

Step	Hyp	Ref	Expression
1		pimltmnf2.1	⊢ Ⅎ 𝑥 𝐹
2		pimltmnf2.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
3		nfcv	⊢ Ⅎ 𝑥 𝐴
4		nfcv	⊢ Ⅎ 𝑦 𝐴
5		nfv	⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑥 ) < -∞
6		nfcv	⊢ Ⅎ 𝑥 𝑦
7	1 6	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 )
8		nfcv	⊢ Ⅎ 𝑥 <
9		nfcv	⊢ Ⅎ 𝑥 -∞
10	7 8 9	nfbr	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 ) < -∞
11		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
12	11	breq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) < -∞ ↔ ( 𝐹 ‘ 𝑦 ) < -∞ ) )
13	3 4 5 10 12	cbvrabw	⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < -∞ } = { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) < -∞ }
14	13	a1i	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < -∞ } = { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) < -∞ } )
15		mnfxr	⊢ -∞ ∈ ℝ*
16	15	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → -∞ ∈ ℝ* )
17	2	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
18	17	rexrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
19	17	mnfltd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → -∞ < ( 𝐹 ‘ 𝑦 ) )
20	16 18 19	xrltled	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → -∞ ≤ ( 𝐹 ‘ 𝑦 ) )
21	16 18	xrlenltd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( -∞ ≤ ( 𝐹 ‘ 𝑦 ) ↔ ¬ ( 𝐹 ‘ 𝑦 ) < -∞ ) )
22	20 21	mpbid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ¬ ( 𝐹 ‘ 𝑦 ) < -∞ )
23	22	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑦 ) < -∞ )
24		rabeq0	⊢ ( { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) < -∞ } = ∅ ↔ ∀ 𝑦 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑦 ) < -∞ )
25	23 24	sylibr	⊢ ( 𝜑 → { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) < -∞ } = ∅ )
26	14 25	eqtrd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < -∞ } = ∅ )