Metamath Proof Explorer


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 ( 𝜑 → { 𝑥𝐴 ∣ ( 𝐹𝑥 ) < 𝐶 } = 𝐴 )