Theorem pimconstlt0

Description: Given a constant function, its preimage with respect to an unbounded below, open interval, with upper bound less than or equal to the constant, is the empty set. Second part of Proposition 121E (a) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	pimconstlt0.x	⊢ Ⅎ 𝑥 𝜑
	pimconstlt0.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	pimconstlt0.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	pimconstlt0.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
	pimconstlt0.l	⊢ ( 𝜑 → 𝐶 ≤ 𝐵 )
Assertion	pimconstlt0	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐶 } = ∅ )

Proof

Step	Hyp	Ref	Expression
1		pimconstlt0.x	⊢ Ⅎ 𝑥 𝜑
2		pimconstlt0.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		pimconstlt0.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4		pimconstlt0.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
5		pimconstlt0.l	⊢ ( 𝜑 → 𝐶 ≤ 𝐵 )
6	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ≤ 𝐵 )
7	3	a1i	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
8	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
9	7 8	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
10	6 9	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ≤ ( 𝐹 ‘ 𝑥 ) )
11	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ* )
12	9 8	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
13	12	rexrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
14	11 13	xrlenltd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ¬ ( 𝐹 ‘ 𝑥 ) < 𝐶 ) )
15	10 14	mpbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ¬ ( 𝐹 ‘ 𝑥 ) < 𝐶 )
16	15	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ¬ ( 𝐹 ‘ 𝑥 ) < 𝐶 ) )
17	1 16	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑥 ) < 𝐶 )
18		rabeq0	⊢ ( { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐶 } = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑥 ) < 𝐶 )
19	17 18	sylibr	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐶 } = ∅ )