Theorem pimgtmnf

Description: Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound -oo , is the whole domain. (Contributed by Glauco Siliprandi, 26-Jun-2021) (Revised by Glauco Siliprandi, 20-Dec-2024)

	Ref	Expression
Hypotheses	pimgtmnf.1	⊢ Ⅎ 𝑥 𝜑
	pimgtmnf.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
Assertion	pimgtmnf	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ -∞ < 𝐵 } = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		pimgtmnf.1	⊢ Ⅎ 𝑥 𝜑
2		pimgtmnf.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3		nfcv	⊢ Ⅎ 𝑥 𝐴
4	1 3 2	pimgtmnff	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ -∞ < 𝐵 } = 𝐴 )