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 ( 𝐶 ⊆ 𝐴 → ( ( 𝑅 ∖ ( 𝐴 × 𝐵 ) ) “ 𝐶 ) = ( ( 𝑅 “ 𝐶 ) ∖ 𝐵 ) )

Proof

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