Theorem pimgtpnf2

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

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

Proof

Step	Hyp	Ref	Expression
1		pimgtpnf2.1	⊢ Ⅎ 𝑥 𝐹
2		pimgtpnf2.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
3		nfcv	⊢ Ⅎ 𝑥 𝐴
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	3 4 5 10 12	cbvrabw	⊢ { 𝑥 ∈ 𝐴 ∣ +∞ < ( 𝐹 ‘ 𝑥 ) } = { 𝑦 ∈ 𝐴 ∣ +∞ < ( 𝐹 ‘ 𝑦 ) }
14	13	a1i	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ +∞ < ( 𝐹 ‘ 𝑥 ) } = { 𝑦 ∈ 𝐴 ∣ +∞ < ( 𝐹 ‘ 𝑦 ) } )
15	2	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
16	15	rexrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
17		pnfxr	⊢ +∞ ∈ ℝ*
18	17	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → +∞ ∈ ℝ* )
19	15	ltpnfd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) < +∞ )
20	16 18 19	xrltled	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ≤ +∞ )
21	16 18	xrlenltd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑦 ) ≤ +∞ ↔ ¬ +∞ < ( 𝐹 ‘ 𝑦 ) ) )
22	20 21	mpbid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ¬ +∞ < ( 𝐹 ‘ 𝑦 ) )
23	22	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ¬ +∞ < ( 𝐹 ‘ 𝑦 ) )
24		rabeq0	⊢ ( { 𝑦 ∈ 𝐴 ∣ +∞ < ( 𝐹 ‘ 𝑦 ) } = ∅ ↔ ∀ 𝑦 ∈ 𝐴 ¬ +∞ < ( 𝐹 ‘ 𝑦 ) )
25	23 24	sylibr	⊢ ( 𝜑 → { 𝑦 ∈ 𝐴 ∣ +∞ < ( 𝐹 ‘ 𝑦 ) } = ∅ )
26	14 25	eqtrd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ +∞ < ( 𝐹 ‘ 𝑥 ) } = ∅ )