Theorem pimgtmnff

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

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

Proof

Step	Hyp	Ref	Expression
1		pimgtmnff.1	⊢ Ⅎ 𝑥 𝜑
2		pimgtmnff.2	⊢ Ⅎ 𝑥 𝐴
3		pimgtmnff.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
4	2	ssrab2f	⊢ { 𝑥 ∈ 𝐴 ∣ -∞ < 𝐵 } ⊆ 𝐴
5	4	a1i	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ -∞ < 𝐵 } ⊆ 𝐴 )
6		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
7		mnflt	⊢ ( 𝐵 ∈ ℝ → -∞ < 𝐵 )
8	3 7	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -∞ < 𝐵 )
9	6 8	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐴 ∧ -∞ < 𝐵 ) )
10		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ -∞ < 𝐵 } ↔ ( 𝑥 ∈ 𝐴 ∧ -∞ < 𝐵 ) )
11	9 10	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ -∞ < 𝐵 } )
12	11	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ -∞ < 𝐵 } ) )
13	1 12	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ -∞ < 𝐵 } )
14		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ -∞ < 𝐵 }
15	2 14	dfss3f	⊢ ( 𝐴 ⊆ { 𝑥 ∈ 𝐴 ∣ -∞ < 𝐵 } ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ -∞ < 𝐵 } )
16	13 15	sylibr	⊢ ( 𝜑 → 𝐴 ⊆ { 𝑥 ∈ 𝐴 ∣ -∞ < 𝐵 } )
17	5 16	eqssd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ -∞ < 𝐵 } = 𝐴 )