Metamath Proof Explorer

Theorem imadifxp

Description: Image of the difference with a Cartesian product. (Contributed by Thierry Arnoux, 13-Dec-2017)

Ref Expression
Assertion imadifxp 
|- ( C C_ A -> ( ( R \ ( A X. B ) ) " C ) = ( ( R " C ) \ B ) )

Proof

Step Hyp Ref Expression
1 ima0 
 |-  ( ( R \ ( A X. B ) ) " (/) ) = (/)
2 imaeq2 
 |-  ( C = (/) -> ( ( R \ ( A X. B ) ) " C ) = ( ( R \ ( A X. B ) ) " (/) ) )
3 imaeq2 
 |-  ( C = (/) -> ( R " C ) = ( R " (/) ) )
4 ima0 
 |-  ( R " (/) ) = (/)
5 3 4 eqtrdi 
 |-  ( C = (/) -> ( R " C ) = (/) )
6 5 difeq1d 
 |-  ( C = (/) -> ( ( R " C ) \ B ) = ( (/) \ B ) )
7 0dif 
 |-  ( (/) \ B ) = (/)
8 6 7 eqtrdi 
 |-  ( C = (/) -> ( ( R " C ) \ B ) = (/) )
9 1 2 8 3eqtr4a 
 |-  ( C = (/) -> ( ( R \ ( A X. B ) ) " C ) = ( ( R " C ) \ B ) )
10 9 adantl 
 |-  ( ( C C_ A /\ C = (/) ) -> ( ( R \ ( A X. B ) ) " C ) = ( ( R " C ) \ B ) )
11 uncom 
 |-  ( (/) u. ( ( R \ ( A X. B ) ) " C ) ) = ( ( ( R \ ( A X. B ) ) " C ) u. (/) )
12 un0 
 |-  ( ( ( R \ ( A X. B ) ) " C ) u. (/) ) = ( ( R \ ( A X. B ) ) " C )
13 11 12 eqtr2i 
 |-  ( ( R \ ( A X. B ) ) " C ) = ( (/) u. ( ( R \ ( A X. B ) ) " C ) )
14 inundif 
 |-  ( ( R i^i ( A X. B ) ) u. ( R \ ( A X. B ) ) ) = R
15 14 imaeq1i 
 |-  ( ( ( R i^i ( A X. B ) ) u. ( R \ ( A X. B ) ) ) " C ) = ( R " C )
16 imaundir 
 |-  ( ( ( R i^i ( A X. B ) ) u. ( R \ ( A X. B ) ) ) " C ) = ( ( ( R i^i ( A X. B ) ) " C ) u. ( ( R \ ( A X. B ) ) " C ) )
17 15 16 eqtr3i 
 |-  ( R " C ) = ( ( ( R i^i ( A X. B ) ) " C ) u. ( ( R \ ( A X. B ) ) " C ) )
18 17 difeq1i 
 |-  ( ( R " C ) \ B ) = ( ( ( ( R i^i ( A X. B ) ) " C ) u. ( ( R \ ( A X. B ) ) " C ) ) \ B )
19 difundir 
 |-  ( ( ( ( R i^i ( A X. B ) ) " C ) u. ( ( R \ ( A X. B ) ) " C ) ) \ B ) = ( ( ( ( R i^i ( A X. B ) ) " C ) \ B ) u. ( ( ( R \ ( A X. B ) ) " C ) \ B ) )
20 18 19 eqtri 
 |-  ( ( R " C ) \ B ) = ( ( ( ( R i^i ( A X. B ) ) " C ) \ B ) u. ( ( ( R \ ( A X. B ) ) " C ) \ B ) )
21 inss2 
 |-  ( R i^i ( A X. B ) ) C_ ( A X. B )
22 imass1 
 |-  ( ( R i^i ( A X. B ) ) C_ ( A X. B ) -> ( ( R i^i ( A X. B ) ) " C ) C_ ( ( A X. B ) " C ) )
23 ssdif 
 |-  ( ( ( R i^i ( A X. B ) ) " C ) C_ ( ( A X. B ) " C ) -> ( ( ( R i^i ( A X. B ) ) " C ) \ B ) C_ ( ( ( A X. B ) " C ) \ B ) )
24 21 22 23 mp2b 
 |-  ( ( ( R i^i ( A X. B ) ) " C ) \ B ) C_ ( ( ( A X. B ) " C ) \ B )
25 xpima 
 |-  ( ( A X. B ) " C ) = if ( ( A i^i C ) = (/) , (/) , B )
26 incom 
 |-  ( C i^i A ) = ( A i^i C )
27 df-ss 
 |-  ( C C_ A <-> ( C i^i A ) = C )
28 27 biimpi 
 |-  ( C C_ A -> ( C i^i A ) = C )
29 26 28 eqtr3id 
 |-  ( C C_ A -> ( A i^i C ) = C )
30 29 adantl 
 |-  ( ( C =/= (/) /\ C C_ A ) -> ( A i^i C ) = C )
31 simpl 
 |-  ( ( C =/= (/) /\ C C_ A ) -> C =/= (/) )
32 30 31 eqnetrd 
 |-  ( ( C =/= (/) /\ C C_ A ) -> ( A i^i C ) =/= (/) )
33 neneq 
 |-  ( ( A i^i C ) =/= (/) -> -. ( A i^i C ) = (/) )
34 iffalse 
 |-  ( -. ( A i^i C ) = (/) -> if ( ( A i^i C ) = (/) , (/) , B ) = B )
35 32 33 34 3syl 
 |-  ( ( C =/= (/) /\ C C_ A ) -> if ( ( A i^i C ) = (/) , (/) , B ) = B )
36 25 35 syl5eq 
 |-  ( ( C =/= (/) /\ C C_ A ) -> ( ( A X. B ) " C ) = B )
37 36 difeq1d 
 |-  ( ( C =/= (/) /\ C C_ A ) -> ( ( ( A X. B ) " C ) \ B ) = ( B \ B ) )
38 difid 
 |-  ( B \ B ) = (/)
39 37 38 eqtrdi 
 |-  ( ( C =/= (/) /\ C C_ A ) -> ( ( ( A X. B ) " C ) \ B ) = (/) )
40 24 39 sseqtrid 
 |-  ( ( C =/= (/) /\ C C_ A ) -> ( ( ( R i^i ( A X. B ) ) " C ) \ B ) C_ (/) )
41 ss0 
 |-  ( ( ( ( R i^i ( A X. B ) ) " C ) \ B ) C_ (/) -> ( ( ( R i^i ( A X. B ) ) " C ) \ B ) = (/) )
42 40 41 syl 
 |-  ( ( C =/= (/) /\ C C_ A ) -> ( ( ( R i^i ( A X. B ) ) " C ) \ B ) = (/) )
43 df-ima 
 |-  ( ( R \ ( A X. B ) ) " C ) = ran ( ( R \ ( A X. B ) ) |` C )
44 df-res 
 |-  ( ( R \ ( A X. B ) ) |` C ) = ( ( R \ ( A X. B ) ) i^i ( C X. _V ) )
45 44 rneqi 
 |-  ran ( ( R \ ( A X. B ) ) |` C ) = ran ( ( R \ ( A X. B ) ) i^i ( C X. _V ) )
46 43 45 eqtri 
 |-  ( ( R \ ( A X. B ) ) " C ) = ran ( ( R \ ( A X. B ) ) i^i ( C X. _V ) )
47 46 ineq1i 
 |-  ( ( ( R \ ( A X. B ) ) " C ) i^i B ) = ( ran ( ( R \ ( A X. B ) ) i^i ( C X. _V ) ) i^i B )
48 xpss1 
 |-  ( C C_ A -> ( C X. _V ) C_ ( A X. _V ) )
49 sslin 
 |-  ( ( C X. _V ) C_ ( A X. _V ) -> ( ( R \ ( A X. B ) ) i^i ( C X. _V ) ) C_ ( ( R \ ( A X. B ) ) i^i ( A X. _V ) ) )
50 rnss 
 |-  ( ( ( R \ ( A X. B ) ) i^i ( C X. _V ) ) C_ ( ( R \ ( A X. B ) ) i^i ( A X. _V ) ) -> ran ( ( R \ ( A X. B ) ) i^i ( C X. _V ) ) C_ ran ( ( R \ ( A X. B ) ) i^i ( A X. _V ) ) )
51 48 49 50 3syl 
 |-  ( C C_ A -> ran ( ( R \ ( A X. B ) ) i^i ( C X. _V ) ) C_ ran ( ( R \ ( A X. B ) ) i^i ( A X. _V ) ) )
52 ssn0 
 |-  ( ( C C_ A /\ C =/= (/) ) -> A =/= (/) )
53 52 ancoms 
 |-  ( ( C =/= (/) /\ C C_ A ) -> A =/= (/) )
54 inss1 
 |-  ( ( A X. _V ) i^i R ) C_ ( A X. _V )
55 ssdif 
 |-  ( ( ( A X. _V ) i^i R ) C_ ( A X. _V ) -> ( ( ( A X. _V ) i^i R ) \ ( A X. B ) ) C_ ( ( A X. _V ) \ ( A X. B ) ) )
56 54 55 ax-mp 
 |-  ( ( ( A X. _V ) i^i R ) \ ( A X. B ) ) C_ ( ( A X. _V ) \ ( A X. B ) )
57 incom 
 |-  ( ( A X. _V ) i^i ( R \ ( A X. B ) ) ) = ( ( R \ ( A X. B ) ) i^i ( A X. _V ) )
58 indif2 
 |-  ( ( A X. _V ) i^i ( R \ ( A X. B ) ) ) = ( ( ( A X. _V ) i^i R ) \ ( A X. B ) )
59 57 58 eqtr3i 
 |-  ( ( R \ ( A X. B ) ) i^i ( A X. _V ) ) = ( ( ( A X. _V ) i^i R ) \ ( A X. B ) )
60 difxp2 
 |-  ( A X. ( _V \ B ) ) = ( ( A X. _V ) \ ( A X. B ) )
61 56 59 60 3sstr4i 
 |-  ( ( R \ ( A X. B ) ) i^i ( A X. _V ) ) C_ ( A X. ( _V \ B ) )
62 rnss 
 |-  ( ( ( R \ ( A X. B ) ) i^i ( A X. _V ) ) C_ ( A X. ( _V \ B ) ) -> ran ( ( R \ ( A X. B ) ) i^i ( A X. _V ) ) C_ ran ( A X. ( _V \ B ) ) )
63 61 62 mp1i 
 |-  ( A =/= (/) -> ran ( ( R \ ( A X. B ) ) i^i ( A X. _V ) ) C_ ran ( A X. ( _V \ B ) ) )
64 rnxp 
 |-  ( A =/= (/) -> ran ( A X. ( _V \ B ) ) = ( _V \ B ) )
65 63 64 sseqtrd 
 |-  ( A =/= (/) -> ran ( ( R \ ( A X. B ) ) i^i ( A X. _V ) ) C_ ( _V \ B ) )
66 disj2 
 |-  ( ( ran ( ( R \ ( A X. B ) ) i^i ( A X. _V ) ) i^i B ) = (/) <-> ran ( ( R \ ( A X. B ) ) i^i ( A X. _V ) ) C_ ( _V \ B ) )
67 65 66 sylibr 
 |-  ( A =/= (/) -> ( ran ( ( R \ ( A X. B ) ) i^i ( A X. _V ) ) i^i B ) = (/) )
68 53 67 syl 
 |-  ( ( C =/= (/) /\ C C_ A ) -> ( ran ( ( R \ ( A X. B ) ) i^i ( A X. _V ) ) i^i B ) = (/) )
69 ssdisj 
 |-  ( ( ran ( ( R \ ( A X. B ) ) i^i ( C X. _V ) ) C_ ran ( ( R \ ( A X. B ) ) i^i ( A X. _V ) ) /\ ( ran ( ( R \ ( A X. B ) ) i^i ( A X. _V ) ) i^i B ) = (/) ) -> ( ran ( ( R \ ( A X. B ) ) i^i ( C X. _V ) ) i^i B ) = (/) )
70 51 68 69 syl2an2 
 |-  ( ( C =/= (/) /\ C C_ A ) -> ( ran ( ( R \ ( A X. B ) ) i^i ( C X. _V ) ) i^i B ) = (/) )
71 47 70 syl5eq 
 |-  ( ( C =/= (/) /\ C C_ A ) -> ( ( ( R \ ( A X. B ) ) " C ) i^i B ) = (/) )
72 disj3 
 |-  ( ( ( ( R \ ( A X. B ) ) " C ) i^i B ) = (/) <-> ( ( R \ ( A X. B ) ) " C ) = ( ( ( R \ ( A X. B ) ) " C ) \ B ) )
73 71 72 sylib 
 |-  ( ( C =/= (/) /\ C C_ A ) -> ( ( R \ ( A X. B ) ) " C ) = ( ( ( R \ ( A X. B ) ) " C ) \ B ) )
74 73 eqcomd 
 |-  ( ( C =/= (/) /\ C C_ A ) -> ( ( ( R \ ( A X. B ) ) " C ) \ B ) = ( ( R \ ( A X. B ) ) " C ) )
75 42 74 uneq12d 
 |-  ( ( C =/= (/) /\ C C_ A ) -> ( ( ( ( R i^i ( A X. B ) ) " C ) \ B ) u. ( ( ( R \ ( A X. B ) ) " C ) \ B ) ) = ( (/) u. ( ( R \ ( A X. B ) ) " C ) ) )
76 20 75 syl5eq 
 |-  ( ( C =/= (/) /\ C C_ A ) -> ( ( R " C ) \ B ) = ( (/) u. ( ( R \ ( A X. B ) ) " C ) ) )
77 13 76 eqtr4id 
 |-  ( ( C =/= (/) /\ C C_ A ) -> ( ( R \ ( A X. B ) ) " C ) = ( ( R " C ) \ B ) )
78 77 ancoms 
 |-  ( ( C C_ A /\ C =/= (/) ) -> ( ( R \ ( A X. B ) ) " C ) = ( ( R " C ) \ B ) )
79 10 78 pm2.61dane 
 |-  ( C C_ A -> ( ( R \ ( A X. B ) ) " C ) = ( ( R " C ) \ B ) )