Theorem pimltpnf2

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	pimltpnf2.1	⊢ Ⅎ 𝑥 𝐹
	pimltpnf2.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
Assertion	pimltpnf2	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < +∞ } = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		pimltpnf2.1	⊢ Ⅎ 𝑥 𝐹
2		pimltpnf2.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
3		nfcv	⊢ Ⅎ 𝑥 𝐴
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	3 4 5 10 12	cbvrabw	⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < +∞ } = { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) < +∞ }
14	13	a1i	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < +∞ } = { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) < +∞ } )
15		nfv	⊢ Ⅎ 𝑦 𝜑
16	2	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
17	15 16	pimltpnf	⊢ ( 𝜑 → { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) < +∞ } = 𝐴 )
18	14 17	eqtrd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < +∞ } = 𝐴 )