Theorem pimgtmnff 44895

Description: Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound -∞, is the whole domain. (Contributed by Glauco Siliprandi, 20-Dec-2024.)

Hypotheses

Ref	Expression
pimgtmnff.1	⊢ Ⅎ𝑥𝜑
pimgtmnff.2	⊢ Ⅎ𝑥𝐴
pimgtmnff.3	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
pimgtmnff	⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ -∞ < 𝐵} = 𝐴)

Proof of Theorem pimgtmnff

Step	Hyp	Ref	Expression
1		pimgtmnff.2	. . . 4 ⊢ Ⅎ𝑥𝐴
2	1	ssrab2f 43269	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ -∞ < 𝐵} ⊆ 𝐴
3	2	a1i 11	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ -∞ < 𝐵} ⊆ 𝐴)
4		pimgtmnff.1	. . . 4 ⊢ Ⅎ𝑥𝜑
5		simpr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
6		pimgtmnff.3	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)
7		mnflt 13036	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ → -∞ < 𝐵)
8	6, 7	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -∞ < 𝐵)
9	5, 8	jca 512	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 ∧ -∞ < 𝐵))
10		rabid 3425	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ -∞ < 𝐵} ↔ (𝑥 ∈ 𝐴 ∧ -∞ < 𝐵))
11	9, 10	sylibr 233	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ -∞ < 𝐵})
12	11	ex 413	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ -∞ < 𝐵}))
13	4, 12	ralrimi 3238	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ -∞ < 𝐵})
14		nfrab1 3424	. . . 4 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ -∞ < 𝐵}
15	1, 14	dfss3f 3933	. . 3 ⊢ (𝐴 ⊆ {𝑥 ∈ 𝐴 ∣ -∞ < 𝐵} ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ -∞ < 𝐵})
16	13, 15	sylibr 233	. 2 ⊢ (𝜑 → 𝐴 ⊆ {𝑥 ∈ 𝐴 ∣ -∞ < 𝐵})
17	3, 16	eqssd 3959	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ -∞ < 𝐵} = 𝐴)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541  Ⅎwnf 1785   ∈ wcel 2106  Ⅎwnfc 2885  ∀wral 3062  {crab 3405   ⊆ wss 3908   class class class wbr 5103  ℝcr 11046  -∞cmnf 11183   < clt 11185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7668  ax-cnex 11103

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-opab 5166  df-xp 5637  df-pnf 11187  df-mnf 11188  df-xr 11189  df-ltxr 11190

This theorem is referenced by:  pimgtmnf  44896