Theorem pimltpnf

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, 26-Jun-2021)

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

Proof

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