Theorem pimltpnf2f

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

	Ref	Expression
Hypotheses	pimltpnf2f.1	⊢ Ⅎ 𝑥 𝐹
	pimltpnf2f.2	⊢ Ⅎ 𝑥 𝐴
	pimltpnf2f.3	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
Assertion	pimltpnf2f	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < +∞ } = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		pimltpnf2f.1	⊢ Ⅎ 𝑥 𝐹
2		pimltpnf2f.2	⊢ Ⅎ 𝑥 𝐴
3		pimltpnf2f.3	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
4		nfcv	⊢ Ⅎ 𝑦 𝐴
5		nfv	⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑥 ) < +∞
6		nfcv	⊢ Ⅎ 𝑥 𝑦
7	1 6	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 )
8		nfcv	⊢ Ⅎ 𝑥 <
9		nfcv	⊢ Ⅎ 𝑥 +∞
10	7 8 9	nfbr	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 ) < +∞
11		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
12	11	breq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) < +∞ ↔ ( 𝐹 ‘ 𝑦 ) < +∞ ) )
13	2 4 5 10 12	cbvrabw	⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < +∞ } = { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) < +∞ }
14		nfv	⊢ Ⅎ 𝑦 𝜑
15	3	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
16	14 15	pimltpnf	⊢ ( 𝜑 → { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) < +∞ } = 𝐴 )
17	13 16	eqtrid	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < +∞ } = 𝐴 )