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 
|- F/ x ph
pimxrneun.2 
|- ( ( ph /\ x e. A ) -> B e. RR* )
pimxrneun.3 
|- ( ( ph /\ x e. A ) -> C e. RR* )
Assertion pimxrneun 
|- ( ph -> { x e. A | B =/= C } = ( { x e. A | B < C } u. { x e. A | C < B } ) )

Proof

Step Hyp Ref Expression
1 pimxrneun.1 
 |-  F/ x ph
2 pimxrneun.2 
 |-  ( ( ph /\ x e. A ) -> B e. RR* )
3 pimxrneun.3 
 |-  ( ( ph /\ x e. A ) -> C e. RR* )
4 nfrab1 
 |-  F/_ x { x e. A | B < C }
5 nfrab1 
 |-  F/_ x { x e. A | C < B }
6 4 5 nfun 
 |-  F/_ x ( { x e. A | B < C } u. { x e. A | C < B } )
7 simpl 
 |-  ( ( x e. A /\ B < C ) -> x e. A )
8 simpr 
 |-  ( ( x e. A /\ B < C ) -> B < C )
9 7 8 jca 
 |-  ( ( x e. A /\ B < C ) -> ( x e. A /\ B < C ) )
10 rabid 
 |-  ( x e. { x e. A | B < C } <-> ( x e. A /\ B < C ) )
11 9 10 sylibr 
 |-  ( ( x e. A /\ B < C ) -> x e. { x e. A | B < C } )
12 11 adantll 
 |-  ( ( ( ph /\ x e. A ) /\ B < C ) -> x e. { x e. A | B < C } )
13 elun1 
 |-  ( x e. { x e. A | B < C } -> x e. ( { x e. A | B < C } u. { x e. A | C < B } ) )
14 12 13 syl 
 |-  ( ( ( ph /\ x e. A ) /\ B < C ) -> x e. ( { x e. A | B < C } u. { x e. A | C < B } ) )
15 14 3adantl3 
 |-  ( ( ( ph /\ x e. A /\ B =/= C ) /\ B < C ) -> x e. ( { x e. A | B < C } u. { x e. A | C < B } ) )
16 3simpa 
 |-  ( ( ph /\ x e. A /\ B =/= C ) -> ( ph /\ x e. A ) )
17 16 adantr 
 |-  ( ( ( ph /\ x e. A /\ B =/= C ) /\ -. B < C ) -> ( ph /\ x e. A ) )
18 3 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ -. B < C ) -> C e. RR* )
19 18 3adantl3 
 |-  ( ( ( ph /\ x e. A /\ B =/= C ) /\ -. B < C ) -> C e. RR* )
20 2 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ -. B < C ) -> B e. RR* )
21 20 3adantl3 
 |-  ( ( ( ph /\ x e. A /\ B =/= C ) /\ -. B < C ) -> B e. RR* )
22 simpr 
 |-  ( ( ( ph /\ x e. A /\ B =/= C ) /\ -. B < C ) -> -. B < C )
23 19 21 22 xrnltled 
 |-  ( ( ( ph /\ x e. A /\ B =/= C ) /\ -. B < C ) -> C <_ B )
24 necom 
 |-  ( B =/= C <-> C =/= B )
25 24 birani 
 |-  ( ( B =/= C /\ -. B < C ) -> C =/= B )
26 25 3ad2antl3 
 |-  ( ( ( ph /\ x e. A /\ B =/= C ) /\ -. B < C ) -> C =/= B )
27 19 21 23 26 xrleneltd 
 |-  ( ( ( ph /\ x e. A /\ B =/= C ) /\ -. B < C ) -> C < B )
28 id 
 |-  ( ( x e. A /\ C < B ) -> ( x e. A /\ C < B ) )
29 28 adantll 
 |-  ( ( ( ph /\ x e. A ) /\ C < B ) -> ( x e. A /\ C < B ) )
30 rabid 
 |-  ( x e. { x e. A | C < B } <-> ( x e. A /\ C < B ) )
31 29 30 sylibr 
 |-  ( ( ( ph /\ x e. A ) /\ C < B ) -> x e. { x e. A | C < B } )
32 elun2 
 |-  ( x e. { x e. A | C < B } -> x e. ( { x e. A | B < C } u. { x e. A | C < B } ) )
33 31 32 syl 
 |-  ( ( ( ph /\ x e. A ) /\ C < B ) -> x e. ( { x e. A | B < C } u. { x e. A | C < B } ) )
34 17 27 33 syl2anc 
 |-  ( ( ( ph /\ x e. A /\ B =/= C ) /\ -. B < C ) -> x e. ( { x e. A | B < C } u. { x e. A | C < B } ) )
35 15 34 pm2.61dan 
 |-  ( ( ph /\ x e. A /\ B =/= C ) -> x e. ( { x e. A | B < C } u. { x e. A | C < B } ) )
36 1 6 35 rabssd 
 |-  ( ph -> { x e. A | B =/= C } C_ ( { x e. A | B < C } u. { x e. A | C < B } ) )
37 2 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ B < C ) -> B e. RR* )
38 3 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ B < C ) -> C e. RR* )
39 simpr 
 |-  ( ( ( ph /\ x e. A ) /\ B < C ) -> B < C )
40 37 38 39 xrltned 
 |-  ( ( ( ph /\ x e. A ) /\ B < C ) -> B =/= C )
41 40 ex 
 |-  ( ( ph /\ x e. A ) -> ( B < C -> B =/= C ) )
42 1 41 ss2rabdf 
 |-  ( ph -> { x e. A | B < C } C_ { x e. A | B =/= C } )
43 3 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ C < B ) -> C e. RR* )
44 2 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ C < B ) -> B e. RR* )
45 simpr 
 |-  ( ( ( ph /\ x e. A ) /\ C < B ) -> C < B )
46 43 44 45 xrgtned 
 |-  ( ( ( ph /\ x e. A ) /\ C < B ) -> B =/= C )
47 46 ex 
 |-  ( ( ph /\ x e. A ) -> ( C < B -> B =/= C ) )
48 1 47 ss2rabdf 
 |-  ( ph -> { x e. A | C < B } C_ { x e. A | B =/= C } )
49 42 48 unssd 
 |-  ( ph -> ( { x e. A | B < C } u. { x e. A | C < B } ) C_ { x e. A | B =/= C } )
50 36 49 eqssd 
 |-  ( ph -> { x e. A | B =/= C } = ( { x e. A | B < C } u. { x e. A | C < B } ) )