Theorem pimgtmnf2

Description: Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound -oo , is the whole domain. (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		pimgtmnf2.1	⊢ Ⅎ 𝑥 𝐹
2		pimgtmnf2.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
3		ssrab2	⊢ { 𝑥 ∈ 𝐴 ∣ -∞ < ( 𝐹 ‘ 𝑥 ) } ⊆ 𝐴
4	3	a1i	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ -∞ < ( 𝐹 ‘ 𝑥 ) } ⊆ 𝐴 )
5		ssid	⊢ 𝐴 ⊆ 𝐴
6	5	a1i	⊢ ( 𝜑 → 𝐴 ⊆ 𝐴 )
7	2	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
8	7	mnfltd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → -∞ < ( 𝐹 ‘ 𝑦 ) )
9	8	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 -∞ < ( 𝐹 ‘ 𝑦 ) )
10		nfcv	⊢ Ⅎ 𝑥 -∞
11		nfcv	⊢ Ⅎ 𝑥 <
12		nfcv	⊢ Ⅎ 𝑥 𝑦
13	1 12	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 )
14	10 11 13	nfbr	⊢ Ⅎ 𝑥 -∞ < ( 𝐹 ‘ 𝑦 )
15		nfv	⊢ Ⅎ 𝑦 -∞ < ( 𝐹 ‘ 𝑥 )
16		fveq2	⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
17	16	breq2d	⊢ ( 𝑦 = 𝑥 → ( -∞ < ( 𝐹 ‘ 𝑦 ) ↔ -∞ < ( 𝐹 ‘ 𝑥 ) ) )
18	14 15 17	cbvralw	⊢ ( ∀ 𝑦 ∈ 𝐴 -∞ < ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 -∞ < ( 𝐹 ‘ 𝑥 ) )
19	9 18	sylib	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 -∞ < ( 𝐹 ‘ 𝑥 ) )
20	6 19	jca	⊢ ( 𝜑 → ( 𝐴 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 -∞ < ( 𝐹 ‘ 𝑥 ) ) )
21		nfcv	⊢ Ⅎ 𝑥 𝐴
22	21 21	ssrabf	⊢ ( 𝐴 ⊆ { 𝑥 ∈ 𝐴 ∣ -∞ < ( 𝐹 ‘ 𝑥 ) } ↔ ( 𝐴 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 -∞ < ( 𝐹 ‘ 𝑥 ) ) )
23	20 22	sylibr	⊢ ( 𝜑 → 𝐴 ⊆ { 𝑥 ∈ 𝐴 ∣ -∞ < ( 𝐹 ‘ 𝑥 ) } )
24	4 23	eqssd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ -∞ < ( 𝐹 ‘ 𝑥 ) } = 𝐴 )