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)

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

Proof

Step	Hyp	Ref	Expression
1		pimgtmnf.1	⊢ Ⅎ 𝑥 𝜑
2		pimgtmnf.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
4	3 2	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
5	4	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
6	5	breq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( -∞ < 𝐵 ↔ -∞ < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) )
7	1 6	rabbida	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ -∞ < 𝐵 } = { 𝑥 ∈ 𝐴 ∣ -∞ < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) } )
8		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
9		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
10	1 2 9	fmptdf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ )
11	8 10	pimgtmnf2	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ -∞ < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) } = 𝐴 )
12	7 11	eqtrd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ -∞ < 𝐵 } = 𝐴 )