Metamath Proof Explorer


Theorem preimagelt

Description: The preimage of a right-open, unbounded below interval, is the complement of a left-closed unbounded above interval. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses preimagelt.x 𝑥 𝜑
preimagelt.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ* )
preimagelt.c ( 𝜑𝐶 ∈ ℝ* )
Assertion preimagelt ( 𝜑 → ( 𝐴 ∖ { 𝑥𝐴𝐶𝐵 } ) = { 𝑥𝐴𝐵 < 𝐶 } )

Proof

Step Hyp Ref Expression
1 preimagelt.x 𝑥 𝜑
2 preimagelt.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ* )
3 preimagelt.c ( 𝜑𝐶 ∈ ℝ* )
4 nfcv 𝑥 𝐴
5 nfrab1 𝑥 { 𝑥𝐴𝐶𝐵 }
6 4 5 nfdif 𝑥 ( 𝐴 ∖ { 𝑥𝐴𝐶𝐵 } )
7 nfrab1 𝑥 { 𝑥𝐴𝐵 < 𝐶 }
8 eldifi ( 𝑥 ∈ ( 𝐴 ∖ { 𝑥𝐴𝐶𝐵 } ) → 𝑥𝐴 )
9 8 adantl ( ( 𝜑𝑥 ∈ ( 𝐴 ∖ { 𝑥𝐴𝐶𝐵 } ) ) → 𝑥𝐴 )
10 eldifn ( 𝑥 ∈ ( 𝐴 ∖ { 𝑥𝐴𝐶𝐵 } ) → ¬ 𝑥 ∈ { 𝑥𝐴𝐶𝐵 } )
11 8 anim1i ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝑥𝐴𝐶𝐵 } ) ∧ 𝐶𝐵 ) → ( 𝑥𝐴𝐶𝐵 ) )
12 rabid ( 𝑥 ∈ { 𝑥𝐴𝐶𝐵 } ↔ ( 𝑥𝐴𝐶𝐵 ) )
13 11 12 sylibr ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝑥𝐴𝐶𝐵 } ) ∧ 𝐶𝐵 ) → 𝑥 ∈ { 𝑥𝐴𝐶𝐵 } )
14 10 13 mtand ( 𝑥 ∈ ( 𝐴 ∖ { 𝑥𝐴𝐶𝐵 } ) → ¬ 𝐶𝐵 )
15 14 adantl ( ( 𝜑𝑥 ∈ ( 𝐴 ∖ { 𝑥𝐴𝐶𝐵 } ) ) → ¬ 𝐶𝐵 )
16 8 2 sylan2 ( ( 𝜑𝑥 ∈ ( 𝐴 ∖ { 𝑥𝐴𝐶𝐵 } ) ) → 𝐵 ∈ ℝ* )
17 3 adantr ( ( 𝜑𝑥 ∈ ( 𝐴 ∖ { 𝑥𝐴𝐶𝐵 } ) ) → 𝐶 ∈ ℝ* )
18 16 17 xrltnled ( ( 𝜑𝑥 ∈ ( 𝐴 ∖ { 𝑥𝐴𝐶𝐵 } ) ) → ( 𝐵 < 𝐶 ↔ ¬ 𝐶𝐵 ) )
19 15 18 mpbird ( ( 𝜑𝑥 ∈ ( 𝐴 ∖ { 𝑥𝐴𝐶𝐵 } ) ) → 𝐵 < 𝐶 )
20 rabid ( 𝑥 ∈ { 𝑥𝐴𝐵 < 𝐶 } ↔ ( 𝑥𝐴𝐵 < 𝐶 ) )
21 9 19 20 sylanbrc ( ( 𝜑𝑥 ∈ ( 𝐴 ∖ { 𝑥𝐴𝐶𝐵 } ) ) → 𝑥 ∈ { 𝑥𝐴𝐵 < 𝐶 } )
22 rabidim1 ( 𝑥 ∈ { 𝑥𝐴𝐵 < 𝐶 } → 𝑥𝐴 )
23 22 adantl ( ( 𝜑𝑥 ∈ { 𝑥𝐴𝐵 < 𝐶 } ) → 𝑥𝐴 )
24 rabidim2 ( 𝑥 ∈ { 𝑥𝐴𝐵 < 𝐶 } → 𝐵 < 𝐶 )
25 24 adantl ( ( 𝜑𝑥 ∈ { 𝑥𝐴𝐵 < 𝐶 } ) → 𝐵 < 𝐶 )
26 22 2 sylan2 ( ( 𝜑𝑥 ∈ { 𝑥𝐴𝐵 < 𝐶 } ) → 𝐵 ∈ ℝ* )
27 3 adantr ( ( 𝜑𝑥 ∈ { 𝑥𝐴𝐵 < 𝐶 } ) → 𝐶 ∈ ℝ* )
28 26 27 xrltnled ( ( 𝜑𝑥 ∈ { 𝑥𝐴𝐵 < 𝐶 } ) → ( 𝐵 < 𝐶 ↔ ¬ 𝐶𝐵 ) )
29 25 28 mpbid ( ( 𝜑𝑥 ∈ { 𝑥𝐴𝐵 < 𝐶 } ) → ¬ 𝐶𝐵 )
30 29 intnand ( ( 𝜑𝑥 ∈ { 𝑥𝐴𝐵 < 𝐶 } ) → ¬ ( 𝑥𝐴𝐶𝐵 ) )
31 30 12 sylnibr ( ( 𝜑𝑥 ∈ { 𝑥𝐴𝐵 < 𝐶 } ) → ¬ 𝑥 ∈ { 𝑥𝐴𝐶𝐵 } )
32 23 31 eldifd ( ( 𝜑𝑥 ∈ { 𝑥𝐴𝐵 < 𝐶 } ) → 𝑥 ∈ ( 𝐴 ∖ { 𝑥𝐴𝐶𝐵 } ) )
33 21 32 impbida ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∖ { 𝑥𝐴𝐶𝐵 } ) ↔ 𝑥 ∈ { 𝑥𝐴𝐵 < 𝐶 } ) )
34 1 6 7 33 eqrd ( 𝜑 → ( 𝐴 ∖ { 𝑥𝐴𝐶𝐵 } ) = { 𝑥𝐴𝐵 < 𝐶 } )