This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pimxrneun

Description: The preimage of a set of extended reals that does not contain a value C is the union of the preimage of the elements smaller than C and the preimage of the subset of elements larger than C . (Contributed by Glauco Siliprandi, 21-Dec-2024)

Ref Expression
Hypotheses pimxrneun.1 ⊢ Ⅎ 𝑥 𝜑
pimxrneun.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
pimxrneun.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ* )
Assertion pimxrneun ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶 } = ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )

Proof

Step Hyp Ref Expression
1 pimxrneun.1 ⊢ Ⅎ 𝑥 𝜑
2 pimxrneun.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
3 pimxrneun.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ* )
4 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 }
5 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 }
6 4 5 nfun ⊢ Ⅎ 𝑥 ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } )
7 simpl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 < 𝐶 ) → 𝑥 ∈ 𝐴 )
8 simpr ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 < 𝐶 ) → 𝐵 < 𝐶 )
9 7 8 jca ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 < 𝐶 ) → ( 𝑥 ∈ 𝐴 ∧ 𝐵 < 𝐶 ) )
10 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐵 < 𝐶 ) )
11 9 10 sylibr ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 < 𝐶 ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } )
12 11 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 < 𝐶 ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } )
13 elun1 ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
14 12 13 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 < 𝐶 ) → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
15 14 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐵 < 𝐶 ) → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
16 3simpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) → ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) )
17 16 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ¬ 𝐵 < 𝐶 ) → ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) )
18 3 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝐵 < 𝐶 ) → 𝐶 ∈ ℝ* )
19 18 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ¬ 𝐵 < 𝐶 ) → 𝐶 ∈ ℝ* )
20 2 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝐵 < 𝐶 ) → 𝐵 ∈ ℝ* )
21 20 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ¬ 𝐵 < 𝐶 ) → 𝐵 ∈ ℝ* )
22 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ¬ 𝐵 < 𝐶 ) → ¬ 𝐵 < 𝐶 )
23 19 21 22 xrnltled ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ¬ 𝐵 < 𝐶 ) → 𝐶 ≤ 𝐵 )
24 necom ⊢ ( 𝐵 ≠ 𝐶 ↔ 𝐶 ≠ 𝐵 )
25 24 biimpi ⊢ ( 𝐵 ≠ 𝐶 → 𝐶 ≠ 𝐵 )
26 25 adantr ⊢ ( ( 𝐵 ≠ 𝐶 ∧ ¬ 𝐵 < 𝐶 ) → 𝐶 ≠ 𝐵 )
27 26 3ad2antl3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ¬ 𝐵 < 𝐶 ) → 𝐶 ≠ 𝐵 )
28 19 21 23 27 xrleneltd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ¬ 𝐵 < 𝐶 ) → 𝐶 < 𝐵 )
29 id ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 < 𝐵 ) → ( 𝑥 ∈ 𝐴 ∧ 𝐶 < 𝐵 ) )
30 29 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → ( 𝑥 ∈ 𝐴 ∧ 𝐶 < 𝐵 ) )
31 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐶 < 𝐵 ) )
32 30 31 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } )
33 elun2 ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
34 32 33 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
35 17 28 34 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ∧ ¬ 𝐵 < 𝐶 ) → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
36 15 35 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) → 𝑥 ∈ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
37 1 6 36 rabssd ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶 } ⊆ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )
38 2 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 < 𝐶 ) → 𝐵 ∈ ℝ* )
39 3 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 < 𝐶 ) → 𝐶 ∈ ℝ* )
40 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 < 𝐶 ) → 𝐵 < 𝐶 )
41 38 39 40 xrltned ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 < 𝐶 ) → 𝐵 ≠ 𝐶 )
42 41 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 < 𝐶 → 𝐵 ≠ 𝐶 ) )
43 1 42 ss2rabdf ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶 } )
44 3 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → 𝐶 ∈ ℝ* )
45 2 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → 𝐵 ∈ ℝ* )
46 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → 𝐶 < 𝐵 )
47 44 45 46 xrgtned ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 < 𝐵 ) → 𝐵 ≠ 𝐶 )
48 47 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 < 𝐵 → 𝐵 ≠ 𝐶 ) )
49 1 48 ss2rabdf ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶 } )
50 43 49 unssd ⊢ ( 𝜑 → ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶 } )
51 37 50 eqssd ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶 } = ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵 } ) )