Theorem pimgtpnf2f

Description: Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound +oo , is the empty set. (Contributed by Glauco Siliprandi, 15-Dec-2021)

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

Proof

Step	Hyp	Ref	Expression
1		pimgtpnf2f.1	⊢ Ⅎ 𝑥 𝐹
2		pimgtpnf2f.2	⊢ Ⅎ 𝑥 𝐴
3		pimgtpnf2f.3	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
4		nfcv	⊢ Ⅎ 𝑦 𝐴
5		nfv	⊢ Ⅎ 𝑦 +∞ < ( 𝐹 ‘ 𝑥 )
6		nfcv	⊢ Ⅎ 𝑥 +∞
7		nfcv	⊢ Ⅎ 𝑥 <
8		nfcv	⊢ Ⅎ 𝑥 𝑦
9	1 8	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 )
10	6 7 9	nfbr	⊢ Ⅎ 𝑥 +∞ < ( 𝐹 ‘ 𝑦 )
11		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
12	11	breq2d	⊢ ( 𝑥 = 𝑦 → ( +∞ < ( 𝐹 ‘ 𝑥 ) ↔ +∞ < ( 𝐹 ‘ 𝑦 ) ) )
13	2 4 5 10 12	cbvrabw	⊢ { 𝑥 ∈ 𝐴 ∣ +∞ < ( 𝐹 ‘ 𝑥 ) } = { 𝑦 ∈ 𝐴 ∣ +∞ < ( 𝐹 ‘ 𝑦 ) }
14	3	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
15	14	rexrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
16	15	pnfged	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ≤ +∞ )
17		pnfxr	⊢ +∞ ∈ ℝ*
18	17	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → +∞ ∈ ℝ* )
19	15 18	xrlenltd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑦 ) ≤ +∞ ↔ ¬ +∞ < ( 𝐹 ‘ 𝑦 ) ) )
20	16 19	mpbid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ¬ +∞ < ( 𝐹 ‘ 𝑦 ) )
21	20	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ¬ +∞ < ( 𝐹 ‘ 𝑦 ) )
22		rabeq0	⊢ ( { 𝑦 ∈ 𝐴 ∣ +∞ < ( 𝐹 ‘ 𝑦 ) } = ∅ ↔ ∀ 𝑦 ∈ 𝐴 ¬ +∞ < ( 𝐹 ‘ 𝑦 ) )
23	21 22	sylibr	⊢ ( 𝜑 → { 𝑦 ∈ 𝐴 ∣ +∞ < ( 𝐹 ‘ 𝑦 ) } = ∅ )
24	13 23	eqtrid	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ +∞ < ( 𝐹 ‘ 𝑥 ) } = ∅ )