Theorem pimltmnf2f

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, 15-Dec-2024)

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

Proof

Step	Hyp	Ref	Expression
1		pimltmnf2f.1	⊢ Ⅎ 𝑥 𝐹
2		pimltmnf2f.2	⊢ Ⅎ 𝑥 𝐴
3		pimltmnf2f.3	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
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	2 4 5 10 12	cbvrabw	⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < -∞ } = { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) < -∞ }
14	3	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
15	14	rexrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
16	15	mnfled	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → -∞ ≤ ( 𝐹 ‘ 𝑦 ) )
17		mnfxr	⊢ -∞ ∈ ℝ*
18	17	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → -∞ ∈ ℝ* )
19	18 15	xrlenltd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( -∞ ≤ ( 𝐹 ‘ 𝑦 ) ↔ ¬ ( 𝐹 ‘ 𝑦 ) < -∞ ) )
20	16 19	mpbid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ¬ ( 𝐹 ‘ 𝑦 ) < -∞ )
21	20	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑦 ) < -∞ )
22		rabeq0	⊢ ( { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) < -∞ } = ∅ ↔ ∀ 𝑦 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑦 ) < -∞ )
23	21 22	sylibr	⊢ ( 𝜑 → { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) < -∞ } = ∅ )
24	13 23	eqtrid	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < -∞ } = ∅ )