Metamath Proof Explorer

Theorem pimrecltpos

Description: The preimage of an unbounded below, open interval, with positive upper bound, for the reciprocal function. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses pimrecltpos.x ⊢ Ⅎ 𝑥 𝜑
pimrecltpos.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
pimrecltpos.n ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≠ 0 )
pimrecltpos.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
Assertion pimrecltpos ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } = ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) )

Proof

Step Hyp Ref Expression
1 pimrecltpos.x ⊢ Ⅎ 𝑥 𝜑
2 pimrecltpos.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3 pimrecltpos.n ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≠ 0 )
4 pimrecltpos.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
5 rabidim1 ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } → 𝑥 ∈ 𝐴 )
6 5 adantr ⊢ ( ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ∧ 𝐵 < 0 ) → 𝑥 ∈ 𝐴 )
7 simpr ⊢ ( ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ∧ 𝐵 < 0 ) → 𝐵 < 0 )
8 6 7 jca ⊢ ( ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ∧ 𝐵 < 0 ) → ( 𝑥 ∈ 𝐴 ∧ 𝐵 < 0 ) )
9 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐵 < 0 ) )
10 8 9 sylibr ⊢ ( ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ∧ 𝐵 < 0 ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } )
11 elun2 ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) )
12 10 11 syl ⊢ ( ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ∧ 𝐵 < 0 ) → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) )
13 12 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) ∧ 𝐵 < 0 ) → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) )
14 0red ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) ∧ ¬ 𝐵 < 0 ) → 0 ∈ ℝ )
15 5 2 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) → 𝐵 ∈ ℝ )
16 15 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) ∧ ¬ 𝐵 < 0 ) → 𝐵 ∈ ℝ )
17 5 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) → 𝑥 ∈ 𝐴 )
18 3 necomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≠ 𝐵 )
19 17 18 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) → 0 ≠ 𝐵 )
20 19 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) ∧ ¬ 𝐵 < 0 ) → 0 ≠ 𝐵 )
21 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) ∧ ¬ 𝐵 < 0 ) → ¬ 𝐵 < 0 )
22 14 16 20 21 lttri5d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) ∧ ¬ 𝐵 < 0 ) → 0 < 𝐵 )
23 17 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) ∧ 0 < 𝐵 ) → 𝑥 ∈ 𝐴 )
24 15 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) ∧ 0 < 𝐵 ) → 𝐵 ∈ ℝ )
25 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) ∧ 0 < 𝐵 ) → 0 < 𝐵 )
26 24 25 elrpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) ∧ 0 < 𝐵 ) → 𝐵 ∈ ℝ+ )
27 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) ∧ 0 < 𝐵 ) → 𝐶 ∈ ℝ+ )
28 rabidim2 ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } → ( 1 / 𝐵 ) < 𝐶 )
29 28 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) ∧ 0 < 𝐵 ) → ( 1 / 𝐵 ) < 𝐶 )
30 26 27 29 ltrec1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) ∧ 0 < 𝐵 ) → ( 1 / 𝐶 ) < 𝐵 )
31 23 30 jca ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) ∧ 0 < 𝐵 ) → ( 𝑥 ∈ 𝐴 ∧ ( 1 / 𝐶 ) < 𝐵 ) )
32 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ↔ ( 𝑥 ∈ 𝐴 ∧ ( 1 / 𝐶 ) < 𝐵 ) )
33 31 32 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) ∧ 0 < 𝐵 ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } )
34 elun1 ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) )
35 33 34 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) ∧ 0 < 𝐵 ) → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) )
36 22 35 syldan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) ∧ ¬ 𝐵 < 0 ) → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) )
37 13 36 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) )
38 37 ex ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) ) )
39 32 simplbi ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } → 𝑥 ∈ 𝐴 )
40 39 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ) → 𝑥 ∈ 𝐴 )
41 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ) → 𝐶 ∈ ℝ+ )
42 40 2 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ) → 𝐵 ∈ ℝ )
43 0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ) → 0 ∈ ℝ )
44 41 rprecred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ) → ( 1 / 𝐶 ) ∈ ℝ )
45 4 rpred ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
46 4 rpgt0d ⊢ ( 𝜑 → 0 < 𝐶 )
47 45 46 recgt0d ⊢ ( 𝜑 → 0 < ( 1 / 𝐶 ) )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ) → 0 < ( 1 / 𝐶 ) )
49 32 simprbi ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } → ( 1 / 𝐶 ) < 𝐵 )
50 49 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ) → ( 1 / 𝐶 ) < 𝐵 )
51 43 44 42 48 50 lttrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ) → 0 < 𝐵 )
52 42 51 elrpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ) → 𝐵 ∈ ℝ+ )
53 41 52 50 ltrec1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ) → ( 1 / 𝐵 ) < 𝐶 )
54 40 53 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ) → ( 𝑥 ∈ 𝐴 ∧ ( 1 / 𝐵 ) < 𝐶 ) )
55 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ↔ ( 𝑥 ∈ 𝐴 ∧ ( 1 / 𝐵 ) < 𝐶 ) )
56 54 55 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } )
57 56 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } )
58 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) ) ∧ ¬ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ) → 𝜑 )
59 elunnel1 ⊢ ( ( 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) ∧ ¬ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } )
60 59 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) ) ∧ ¬ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } )
61 9 simplbi ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } → 𝑥 ∈ 𝐴 )
62 61 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) → 𝑥 ∈ 𝐴 )
63 2 3 rereccld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 1 / 𝐵 ) ∈ ℝ )
64 62 63 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) → ( 1 / 𝐵 ) ∈ ℝ )
65 0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) → 0 ∈ ℝ )
66 45 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) → 𝐶 ∈ ℝ )
67 62 2 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) → 𝐵 ∈ ℝ )
68 9 simprbi ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } → 𝐵 < 0 )
69 68 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) → 𝐵 < 0 )
70 67 69 reclt0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) → ( 1 / 𝐵 ) < 0 )
71 46 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) → 0 < 𝐶 )
72 64 65 66 70 71 lttrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) → ( 1 / 𝐵 ) < 𝐶 )
73 62 72 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) → ( 𝑥 ∈ 𝐴 ∧ ( 1 / 𝐵 ) < 𝐶 ) )
74 73 55 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } )
75 58 60 74 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) ) ∧ ¬ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } )
76 57 75 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } )
77 76 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ) )
78 38 77 impbid ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ↔ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) ) )
79 1 78 alrimi ⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ↔ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) ) )
80 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 }
81 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 }
82 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 }
83 81 82 nfun ⊢ Ⅎ 𝑥 ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } )
84 80 83 cleqf ⊢ ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } = ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } ↔ 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) ) )
85 79 84 sylibr ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } = ( { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐶 ) < 𝐵 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 0 } ) )