Theorem pimltpnff

Description: Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound +oo , is the whole domain. (Contributed by Glauco Siliprandi, 20-Dec-2024)

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

Proof

Step	Hyp	Ref	Expression
1		pimltpnff.1	⊢ Ⅎ 𝑥 𝜑
2		pimltpnff.2	⊢ Ⅎ 𝑥 𝐴
3		pimltpnff.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
4	2	ssrab2f	⊢ { 𝑥 ∈ 𝐴 ∣ 𝐵 < +∞ } ⊆ 𝐴
5	4	a1i	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 < +∞ } ⊆ 𝐴 )
6		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
7		ltpnf	⊢ ( 𝐵 ∈ ℝ → 𝐵 < +∞ )
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	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 < +∞ } = 𝐴 )