Theorem pimconstlt1

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

	Ref	Expression
Hypotheses	pimconstlt1.1	⊢ Ⅎ 𝑥 𝜑
	pimconstlt1.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	pimconstlt1.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	pimconstlt1.4	⊢ ( 𝜑 → 𝐵 < 𝐶 )
Assertion	pimconstlt1	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐶 } = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		pimconstlt1.1	⊢ Ⅎ 𝑥 𝜑
2		pimconstlt1.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		pimconstlt1.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4		pimconstlt1.4	⊢ ( 𝜑 → 𝐵 < 𝐶 )
5		ssrab2	⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐶 } ⊆ 𝐴
6	5	a1i	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐶 } ⊆ 𝐴 )
7		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
8	3	a1i	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
9	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
10	8 9	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
11	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 < 𝐶 )
12	10 11	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) < 𝐶 )
13	7 12	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) < 𝐶 ) )
14		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐶 } ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) < 𝐶 ) )
15	13 14	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐶 } )
16	15	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐶 } ) )
17	1 16	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐶 } )
18		nfcv	⊢ Ⅎ 𝑥 𝐴
19		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐶 }
20	18 19	dfss3f	⊢ ( 𝐴 ⊆ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐶 } ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐶 } )
21	17 20	sylibr	⊢ ( 𝜑 → 𝐴 ⊆ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐶 } )
22	6 21	eqssd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝐶 } = 𝐴 )