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 biimpi 
 |-  ( B =/= C -> C =/= B )
26 25 adantr 
 |-  ( ( B =/= C /\ -. B < C ) -> C =/= B )
27 26 3ad2antl3 
 |-  ( ( ( ph /\ x e. A /\ B =/= C ) /\ -. B < C ) -> C =/= B )
28 19 21 23 27 xrleneltd 
 |-  ( ( ( ph /\ x e. A /\ B =/= C ) /\ -. B < C ) -> C < B )
29 id 
 |-  ( ( x e. A /\ C < B ) -> ( x e. A /\ C < B ) )
30 29 adantll 
 |-  ( ( ( ph /\ x e. A ) /\ C < B ) -> ( x e. A /\ C < B ) )
31 rabid 
 |-  ( x e. { x e. A | C < B } <-> ( x e. A /\ C < B ) )
32 30 31 sylibr 
 |-  ( ( ( ph /\ x e. A ) /\ C < B ) -> x e. { x e. A | C < B } )
33 elun2 
 |-  ( x e. { x e. A | C < B } -> x e. ( { x e. A | B < C } u. { x e. A | C < B } ) )
34 32 33 syl 
 |-  ( ( ( ph /\ x e. A ) /\ C < B ) -> x e. ( { x e. A | B < C } u. { x e. A | C < B } ) )
35 17 28 34 syl2anc 
 |-  ( ( ( ph /\ x e. A /\ B =/= C ) /\ -. B < C ) -> x e. ( { x e. A | B < C } u. { x e. A | C < B } ) )
36 15 35 pm2.61dan 
 |-  ( ( ph /\ x e. A /\ B =/= C ) -> x e. ( { x e. A | B < C } u. { x e. A | C < B } ) )
37 1 6 36 rabssd 
 |-  ( ph -> { x e. A | B =/= C } C_ ( { x e. A | B < C } u. { x e. A | C < B } ) )
38 2 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ B < C ) -> B e. RR* )
39 3 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ B < C ) -> C e. RR* )
40 simpr 
 |-  ( ( ( ph /\ x e. A ) /\ B < C ) -> B < C )
41 38 39 40 xrltned 
 |-  ( ( ( ph /\ x e. A ) /\ B < C ) -> B =/= C )
42 41 ex 
 |-  ( ( ph /\ x e. A ) -> ( B < C -> B =/= C ) )
43 1 42 ss2rabdf 
 |-  ( ph -> { x e. A | B < C } C_ { x e. A | B =/= C } )
44 3 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ C < B ) -> C e. RR* )
45 2 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ C < B ) -> B e. RR* )
46 simpr 
 |-  ( ( ( ph /\ x e. A ) /\ C < B ) -> C < B )
47 44 45 46 xrgtned 
 |-  ( ( ( ph /\ x e. A ) /\ C < B ) -> B =/= C )
48 47 ex 
 |-  ( ( ph /\ x e. A ) -> ( C < B -> B =/= C ) )
49 1 48 ss2rabdf 
 |-  ( ph -> { x e. A | C < B } C_ { x e. A | B =/= C } )
50 43 49 unssd 
 |-  ( ph -> ( { x e. A | B < C } u. { x e. A | C < B } ) C_ { x e. A | B =/= C } )
51 37 50 eqssd 
 |-  ( ph -> { x e. A | B =/= C } = ( { x e. A | B < C } u. { x e. A | C < B } ) )