Proof of Theorem imadifxp
Step | Hyp | Ref
| Expression |
1 | | ima0 5938 |
. . . 4
⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ ∅) =
∅ |
2 | | imaeq2 5918 |
. . . 4
⊢ (𝐶 = ∅ → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 ∖ (𝐴 × 𝐵)) “ ∅)) |
3 | | imaeq2 5918 |
. . . . . . 7
⊢ (𝐶 = ∅ → (𝑅 “ 𝐶) = (𝑅 “ ∅)) |
4 | | ima0 5938 |
. . . . . . 7
⊢ (𝑅 “ ∅) =
∅ |
5 | 3, 4 | syl6eq 2869 |
. . . . . 6
⊢ (𝐶 = ∅ → (𝑅 “ 𝐶) = ∅) |
6 | 5 | difeq1d 4095 |
. . . . 5
⊢ (𝐶 = ∅ → ((𝑅 “ 𝐶) ∖ 𝐵) = (∅ ∖ 𝐵)) |
7 | | 0dif 4352 |
. . . . 5
⊢ (∅
∖ 𝐵) =
∅ |
8 | 6, 7 | syl6eq 2869 |
. . . 4
⊢ (𝐶 = ∅ → ((𝑅 “ 𝐶) ∖ 𝐵) = ∅) |
9 | 1, 2, 8 | 3eqtr4a 2879 |
. . 3
⊢ (𝐶 = ∅ → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵)) |
10 | 9 | adantl 482 |
. 2
⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐶 = ∅) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵)) |
11 | | inundif 4423 |
. . . . . . . . 9
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) = 𝑅 |
12 | 11 | imaeq1i 5919 |
. . . . . . . 8
⊢ (((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) “ 𝐶) = (𝑅 “ 𝐶) |
13 | | imaundir 6002 |
. . . . . . . 8
⊢ (((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) “ 𝐶) = (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) |
14 | 12, 13 | eqtr3i 2843 |
. . . . . . 7
⊢ (𝑅 “ 𝐶) = (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) |
15 | 14 | difeq1i 4092 |
. . . . . 6
⊢ ((𝑅 “ 𝐶) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) ∖ 𝐵) |
16 | | difundir 4254 |
. . . . . 6
⊢ ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵)) |
17 | 15, 16 | eqtri 2841 |
. . . . 5
⊢ ((𝑅 “ 𝐶) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵)) |
18 | | inss2 4203 |
. . . . . . . . 9
⊢ (𝑅 ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵) |
19 | | imass1 5957 |
. . . . . . . . 9
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵) → ((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ⊆ ((𝐴 × 𝐵) “ 𝐶)) |
20 | | ssdif 4113 |
. . . . . . . . 9
⊢ (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ⊆ ((𝐴 × 𝐵) “ 𝐶) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵)) |
21 | 18, 19, 20 | mp2b 10 |
. . . . . . . 8
⊢ (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵) |
22 | | xpima 6032 |
. . . . . . . . . . 11
⊢ ((𝐴 × 𝐵) “ 𝐶) = if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) |
23 | | incom 4175 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶) |
24 | | df-ss 3949 |
. . . . . . . . . . . . . . . 16
⊢ (𝐶 ⊆ 𝐴 ↔ (𝐶 ∩ 𝐴) = 𝐶) |
25 | 24 | biimpi 217 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ⊆ 𝐴 → (𝐶 ∩ 𝐴) = 𝐶) |
26 | 23, 25 | syl5eqr 2867 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ⊆ 𝐴 → (𝐴 ∩ 𝐶) = 𝐶) |
27 | 26 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (𝐴 ∩ 𝐶) = 𝐶) |
28 | | simpl 483 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → 𝐶 ≠ ∅) |
29 | 27, 28 | eqnetrd 3080 |
. . . . . . . . . . . 12
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (𝐴 ∩ 𝐶) ≠ ∅) |
30 | | neneq 3019 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∩ 𝐶) ≠ ∅ → ¬ (𝐴 ∩ 𝐶) = ∅) |
31 | | iffalse 4472 |
. . . . . . . . . . . 12
⊢ (¬
(𝐴 ∩ 𝐶) = ∅ → if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) = 𝐵) |
32 | 29, 30, 31 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) = 𝐵) |
33 | 22, 32 | syl5eq 2865 |
. . . . . . . . . 10
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝐴 × 𝐵) “ 𝐶) = 𝐵) |
34 | 33 | difeq1d 4095 |
. . . . . . . . 9
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵) = (𝐵 ∖ 𝐵)) |
35 | | difid 4327 |
. . . . . . . . 9
⊢ (𝐵 ∖ 𝐵) = ∅ |
36 | 34, 35 | syl6eq 2869 |
. . . . . . . 8
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵) = ∅) |
37 | 21, 36 | sseqtrid 4016 |
. . . . . . 7
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ ∅) |
38 | | ss0 4349 |
. . . . . . 7
⊢ ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ ∅ → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ∅) |
39 | 37, 38 | syl 17 |
. . . . . 6
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ∅) |
40 | | df-ima 5561 |
. . . . . . . . . . 11
⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶) |
41 | | df-res 5560 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶) = ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) |
42 | 41 | rneqi 5800 |
. . . . . . . . . . 11
⊢ ran
((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) |
43 | 40, 42 | eqtri 2841 |
. . . . . . . . . 10
⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) |
44 | 43 | ineq1i 4182 |
. . . . . . . . 9
⊢ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵) |
45 | | xpss1 5567 |
. . . . . . . . . . 11
⊢ (𝐶 ⊆ 𝐴 → (𝐶 × V) ⊆ (𝐴 × V)) |
46 | | sslin 4208 |
. . . . . . . . . . 11
⊢ ((𝐶 × V) ⊆ (𝐴 × V) → ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V))) |
47 | | rnss 5802 |
. . . . . . . . . . 11
⊢ (((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V))) |
48 | 45, 46, 47 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝐶 ⊆ 𝐴 → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V))) |
49 | | ssn0 4351 |
. . . . . . . . . . . 12
⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅) → 𝐴 ≠ ∅) |
50 | 49 | ancoms 459 |
. . . . . . . . . . 11
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → 𝐴 ≠ ∅) |
51 | | inss1 4202 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 × V) ∩ 𝑅) ⊆ (𝐴 × V) |
52 | | ssdif 4113 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 × V) ∩ 𝑅) ⊆ (𝐴 × V) → (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵)) ⊆ ((𝐴 × V) ∖ (𝐴 × 𝐵))) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵)) ⊆ ((𝐴 × V) ∖ (𝐴 × 𝐵)) |
54 | | incom 4175 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 × V) ∩ (𝑅 ∖ (𝐴 × 𝐵))) = ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) |
55 | | indif2 4244 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 × V) ∩ (𝑅 ∖ (𝐴 × 𝐵))) = (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵)) |
56 | 54, 55 | eqtr3i 2843 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) = (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵)) |
57 | | difxp2 6016 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 × (V ∖ 𝐵)) = ((𝐴 × V) ∖ (𝐴 × 𝐵)) |
58 | 53, 56, 57 | 3sstr4i 4007 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (𝐴 × (V ∖ 𝐵)) |
59 | | rnss 5802 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (𝐴 × (V ∖ 𝐵)) → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ ran (𝐴 × (V ∖ 𝐵))) |
60 | 58, 59 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝐴 ≠ ∅ → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ ran (𝐴 × (V ∖ 𝐵))) |
61 | | rnxp 6020 |
. . . . . . . . . . . . 13
⊢ (𝐴 ≠ ∅ → ran (𝐴 × (V ∖ 𝐵)) = (V ∖ 𝐵)) |
62 | 60, 61 | sseqtrd 4004 |
. . . . . . . . . . . 12
⊢ (𝐴 ≠ ∅ → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (V ∖ 𝐵)) |
63 | | disj2 4403 |
. . . . . . . . . . . 12
⊢ ((ran
((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅ ↔ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (V ∖ 𝐵)) |
64 | 62, 63 | sylibr 235 |
. . . . . . . . . . 11
⊢ (𝐴 ≠ ∅ → (ran
((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅) |
65 | 50, 64 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅) |
66 | | ssdisj 4405 |
. . . . . . . . . 10
⊢ ((ran
((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∧ (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵) = ∅) |
67 | 48, 65, 66 | syl2an2 682 |
. . . . . . . . 9
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵) = ∅) |
68 | 44, 67 | syl5eq 2865 |
. . . . . . . 8
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = ∅) |
69 | | disj3 4399 |
. . . . . . . 8
⊢ ((((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = ∅ ↔ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵)) |
70 | 68, 69 | sylib 219 |
. . . . . . 7
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵)) |
71 | 70 | eqcomd 2824 |
. . . . . 6
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) |
72 | 39, 71 | uneq12d 4137 |
. . . . 5
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵)) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))) |
73 | 17, 72 | syl5eq 2865 |
. . . 4
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝑅 “ 𝐶) ∖ 𝐵) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))) |
74 | | uncom 4126 |
. . . . 5
⊢ (∅
∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∪ ∅) |
75 | | un0 4341 |
. . . . 5
⊢ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∪ ∅) = ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) |
76 | 74, 75 | eqtr2i 2842 |
. . . 4
⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) |
77 | 73, 76 | syl6reqr 2872 |
. . 3
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵)) |
78 | 77 | ancoms 459 |
. 2
⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵)) |
79 | 10, 78 | pm2.61dane 3101 |
1
⊢ (𝐶 ⊆ 𝐴 → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵)) |