Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  imadifxp Structured version   Visualization version   GIF version

Theorem imadifxp 29721
Description: Image of the difference with a Cartesian product. (Contributed by Thierry Arnoux, 13-Dec-2017.)
Assertion
Ref Expression
imadifxp (𝐶𝐴 → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅𝐶) ∖ 𝐵))

Proof of Theorem imadifxp
StepHypRef Expression
1 ima0 5639 . . . 4 ((𝑅 ∖ (𝐴 × 𝐵)) “ ∅) = ∅
2 imaeq2 5620 . . . 4 (𝐶 = ∅ → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 ∖ (𝐴 × 𝐵)) “ ∅))
3 imaeq2 5620 . . . . . . 7 (𝐶 = ∅ → (𝑅𝐶) = (𝑅 “ ∅))
4 ima0 5639 . . . . . . 7 (𝑅 “ ∅) = ∅
53, 4syl6eq 2810 . . . . . 6 (𝐶 = ∅ → (𝑅𝐶) = ∅)
65difeq1d 3870 . . . . 5 (𝐶 = ∅ → ((𝑅𝐶) ∖ 𝐵) = (∅ ∖ 𝐵))
7 0dif 4120 . . . . 5 (∅ ∖ 𝐵) = ∅
86, 7syl6eq 2810 . . . 4 (𝐶 = ∅ → ((𝑅𝐶) ∖ 𝐵) = ∅)
91, 2, 83eqtr4a 2820 . . 3 (𝐶 = ∅ → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅𝐶) ∖ 𝐵))
109adantl 473 . 2 ((𝐶𝐴𝐶 = ∅) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅𝐶) ∖ 𝐵))
11 inundif 4190 . . . . . . . . 9 ((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) = 𝑅
1211imaeq1i 5621 . . . . . . . 8 (((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) “ 𝐶) = (𝑅𝐶)
13 imaundir 5704 . . . . . . . 8 (((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) “ 𝐶) = (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))
1412, 13eqtr3i 2784 . . . . . . 7 (𝑅𝐶) = (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))
1514difeq1i 3867 . . . . . 6 ((𝑅𝐶) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) ∖ 𝐵)
16 difundir 4023 . . . . . 6 ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵))
1715, 16eqtri 2782 . . . . 5 ((𝑅𝐶) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵))
18 inss2 3977 . . . . . . . . 9 (𝑅 ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵)
19 imass1 5658 . . . . . . . . 9 ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵) → ((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ⊆ ((𝐴 × 𝐵) “ 𝐶))
20 ssdif 3888 . . . . . . . . 9 (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ⊆ ((𝐴 × 𝐵) “ 𝐶) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵))
2118, 19, 20mp2b 10 . . . . . . . 8 (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵)
22 xpima 5734 . . . . . . . . . . 11 ((𝐴 × 𝐵) “ 𝐶) = if((𝐴𝐶) = ∅, ∅, 𝐵)
23 incom 3948 . . . . . . . . . . . . . . 15 (𝐶𝐴) = (𝐴𝐶)
24 df-ss 3729 . . . . . . . . . . . . . . . 16 (𝐶𝐴 ↔ (𝐶𝐴) = 𝐶)
2524biimpi 206 . . . . . . . . . . . . . . 15 (𝐶𝐴 → (𝐶𝐴) = 𝐶)
2623, 25syl5eqr 2808 . . . . . . . . . . . . . 14 (𝐶𝐴 → (𝐴𝐶) = 𝐶)
2726adantl 473 . . . . . . . . . . . . 13 ((𝐶 ≠ ∅ ∧ 𝐶𝐴) → (𝐴𝐶) = 𝐶)
28 simpl 474 . . . . . . . . . . . . 13 ((𝐶 ≠ ∅ ∧ 𝐶𝐴) → 𝐶 ≠ ∅)
2927, 28eqnetrd 2999 . . . . . . . . . . . 12 ((𝐶 ≠ ∅ ∧ 𝐶𝐴) → (𝐴𝐶) ≠ ∅)
30 df-ne 2933 . . . . . . . . . . . . 13 ((𝐴𝐶) ≠ ∅ ↔ ¬ (𝐴𝐶) = ∅)
3130biimpi 206 . . . . . . . . . . . 12 ((𝐴𝐶) ≠ ∅ → ¬ (𝐴𝐶) = ∅)
32 iffalse 4239 . . . . . . . . . . . 12 (¬ (𝐴𝐶) = ∅ → if((𝐴𝐶) = ∅, ∅, 𝐵) = 𝐵)
3329, 31, 323syl 18 . . . . . . . . . . 11 ((𝐶 ≠ ∅ ∧ 𝐶𝐴) → if((𝐴𝐶) = ∅, ∅, 𝐵) = 𝐵)
3422, 33syl5eq 2806 . . . . . . . . . 10 ((𝐶 ≠ ∅ ∧ 𝐶𝐴) → ((𝐴 × 𝐵) “ 𝐶) = 𝐵)
3534difeq1d 3870 . . . . . . . . 9 ((𝐶 ≠ ∅ ∧ 𝐶𝐴) → (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵) = (𝐵𝐵))
36 difid 4091 . . . . . . . . 9 (𝐵𝐵) = ∅
3735, 36syl6eq 2810 . . . . . . . 8 ((𝐶 ≠ ∅ ∧ 𝐶𝐴) → (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵) = ∅)
3821, 37syl5sseq 3794 . . . . . . 7 ((𝐶 ≠ ∅ ∧ 𝐶𝐴) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ ∅)
39 ss0 4117 . . . . . . 7 ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ ∅ → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ∅)
4038, 39syl 17 . . . . . 6 ((𝐶 ≠ ∅ ∧ 𝐶𝐴) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ∅)
41 df-ima 5279 . . . . . . . . . . 11 ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶)
42 df-res 5278 . . . . . . . . . . . 12 ((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶) = ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V))
4342rneqi 5507 . . . . . . . . . . 11 ran ((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V))
4441, 43eqtri 2782 . . . . . . . . . 10 ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V))
4544ineq1i 3953 . . . . . . . . 9 (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵)
46 xpss1 5284 . . . . . . . . . . . 12 (𝐶𝐴 → (𝐶 × V) ⊆ (𝐴 × V))
47 sslin 3982 . . . . . . . . . . . 12 ((𝐶 × V) ⊆ (𝐴 × V) → ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)))
48 rnss 5509 . . . . . . . . . . . 12 (((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)))
4946, 47, 483syl 18 . . . . . . . . . . 11 (𝐶𝐴 → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)))
5049adantl 473 . . . . . . . . . 10 ((𝐶 ≠ ∅ ∧ 𝐶𝐴) → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)))
51 ssn0 4119 . . . . . . . . . . . 12 ((𝐶𝐴𝐶 ≠ ∅) → 𝐴 ≠ ∅)
5251ancoms 468 . . . . . . . . . . 11 ((𝐶 ≠ ∅ ∧ 𝐶𝐴) → 𝐴 ≠ ∅)
53 inss1 3976 . . . . . . . . . . . . . . . 16 ((𝐴 × V) ∩ 𝑅) ⊆ (𝐴 × V)
54 ssdif 3888 . . . . . . . . . . . . . . . 16 (((𝐴 × V) ∩ 𝑅) ⊆ (𝐴 × V) → (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵)) ⊆ ((𝐴 × V) ∖ (𝐴 × 𝐵)))
5553, 54ax-mp 5 . . . . . . . . . . . . . . 15 (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵)) ⊆ ((𝐴 × V) ∖ (𝐴 × 𝐵))
56 incom 3948 . . . . . . . . . . . . . . . 16 ((𝐴 × V) ∩ (𝑅 ∖ (𝐴 × 𝐵))) = ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V))
57 indif2 4013 . . . . . . . . . . . . . . . 16 ((𝐴 × V) ∩ (𝑅 ∖ (𝐴 × 𝐵))) = (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵))
5856, 57eqtr3i 2784 . . . . . . . . . . . . . . 15 ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) = (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵))
59 difxp2 5718 . . . . . . . . . . . . . . 15 (𝐴 × (V ∖ 𝐵)) = ((𝐴 × V) ∖ (𝐴 × 𝐵))
6055, 58, 593sstr4i 3785 . . . . . . . . . . . . . 14 ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (𝐴 × (V ∖ 𝐵))
61 rnss 5509 . . . . . . . . . . . . . 14 (((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (𝐴 × (V ∖ 𝐵)) → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ ran (𝐴 × (V ∖ 𝐵)))
6260, 61mp1i 13 . . . . . . . . . . . . 13 (𝐴 ≠ ∅ → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ ran (𝐴 × (V ∖ 𝐵)))
63 rnxp 5722 . . . . . . . . . . . . 13 (𝐴 ≠ ∅ → ran (𝐴 × (V ∖ 𝐵)) = (V ∖ 𝐵))
6462, 63sseqtrd 3782 . . . . . . . . . . . 12 (𝐴 ≠ ∅ → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (V ∖ 𝐵))
65 disj2 4168 . . . . . . . . . . . 12 ((ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅ ↔ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (V ∖ 𝐵))
6664, 65sylibr 224 . . . . . . . . . . 11 (𝐴 ≠ ∅ → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅)
6752, 66syl 17 . . . . . . . . . 10 ((𝐶 ≠ ∅ ∧ 𝐶𝐴) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅)
68 ssdisj 4170 . . . . . . . . . 10 ((ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∧ (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵) = ∅)
6950, 67, 68syl2anc 696 . . . . . . . . 9 ((𝐶 ≠ ∅ ∧ 𝐶𝐴) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵) = ∅)
7045, 69syl5eq 2806 . . . . . . . 8 ((𝐶 ≠ ∅ ∧ 𝐶𝐴) → (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = ∅)
71 disj3 4164 . . . . . . . 8 ((((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = ∅ ↔ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵))
7270, 71sylib 208 . . . . . . 7 ((𝐶 ≠ ∅ ∧ 𝐶𝐴) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵))
7372eqcomd 2766 . . . . . 6 ((𝐶 ≠ ∅ ∧ 𝐶𝐴) → (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))
7440, 73uneq12d 3911 . . . . 5 ((𝐶 ≠ ∅ ∧ 𝐶𝐴) → ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵)) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)))
7517, 74syl5eq 2806 . . . 4 ((𝐶 ≠ ∅ ∧ 𝐶𝐴) → ((𝑅𝐶) ∖ 𝐵) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)))
76 uncom 3900 . . . . 5 (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∪ ∅)
77 un0 4110 . . . . 5 (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∪ ∅) = ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)
7876, 77eqtr2i 2783 . . . 4 ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))
7975, 78syl6reqr 2813 . . 3 ((𝐶 ≠ ∅ ∧ 𝐶𝐴) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅𝐶) ∖ 𝐵))
8079ancoms 468 . 2 ((𝐶𝐴𝐶 ≠ ∅) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅𝐶) ∖ 𝐵))
8110, 80pm2.61dane 3019 1 (𝐶𝐴 → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅𝐶) ∖ 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383   = wceq 1632  wne 2932  Vcvv 3340  cdif 3712  cun 3713  cin 3714  wss 3715  c0 4058  ifcif 4230   × cxp 5264  ran crn 5267  cres 5268  cima 5269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-xp 5272  df-rel 5273  df-cnv 5274  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator