Proof of Theorem imadifxp
Step | Hyp | Ref
| Expression |
1 | | ima0 5400 |
. . . 4
⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ ∅) =
∅ |
2 | | imaeq2 5381 |
. . . 4
⊢ (𝐶 = ∅ → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 ∖ (𝐴 × 𝐵)) “ ∅)) |
3 | | imaeq2 5381 |
. . . . . . 7
⊢ (𝐶 = ∅ → (𝑅 “ 𝐶) = (𝑅 “ ∅)) |
4 | | ima0 5400 |
. . . . . . 7
⊢ (𝑅 “ ∅) =
∅ |
5 | 3, 4 | syl6eq 2660 |
. . . . . 6
⊢ (𝐶 = ∅ → (𝑅 “ 𝐶) = ∅) |
6 | 5 | difeq1d 3689 |
. . . . 5
⊢ (𝐶 = ∅ → ((𝑅 “ 𝐶) ∖ 𝐵) = (∅ ∖ 𝐵)) |
7 | | 0dif 3929 |
. . . . 5
⊢ (∅
∖ 𝐵) =
∅ |
8 | 6, 7 | syl6eq 2660 |
. . . 4
⊢ (𝐶 = ∅ → ((𝑅 “ 𝐶) ∖ 𝐵) = ∅) |
9 | 1, 2, 8 | 3eqtr4a 2670 |
. . 3
⊢ (𝐶 = ∅ → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵)) |
10 | 9 | adantl 481 |
. 2
⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐶 = ∅) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵)) |
11 | | inundif 3998 |
. . . . . . . . 9
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) = 𝑅 |
12 | 11 | imaeq1i 5382 |
. . . . . . . 8
⊢ (((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) “ 𝐶) = (𝑅 “ 𝐶) |
13 | | imaundir 5465 |
. . . . . . . 8
⊢ (((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) “ 𝐶) = (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) |
14 | 12, 13 | eqtr3i 2634 |
. . . . . . 7
⊢ (𝑅 “ 𝐶) = (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) |
15 | 14 | difeq1i 3686 |
. . . . . 6
⊢ ((𝑅 “ 𝐶) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) ∖ 𝐵) |
16 | | difundir 3839 |
. . . . . 6
⊢ ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵)) |
17 | 15, 16 | eqtri 2632 |
. . . . 5
⊢ ((𝑅 “ 𝐶) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵)) |
18 | | inss2 3796 |
. . . . . . . . 9
⊢ (𝑅 ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵) |
19 | | imass1 5419 |
. . . . . . . . 9
⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵) → ((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ⊆ ((𝐴 × 𝐵) “ 𝐶)) |
20 | | ssdif 3707 |
. . . . . . . . 9
⊢ (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ⊆ ((𝐴 × 𝐵) “ 𝐶) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵)) |
21 | 18, 19, 20 | mp2b 10 |
. . . . . . . 8
⊢ (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵) |
22 | | xpima 5495 |
. . . . . . . . . . 11
⊢ ((𝐴 × 𝐵) “ 𝐶) = if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) |
23 | | incom 3767 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶) |
24 | | df-ss 3554 |
. . . . . . . . . . . . . . . 16
⊢ (𝐶 ⊆ 𝐴 ↔ (𝐶 ∩ 𝐴) = 𝐶) |
25 | 24 | biimpi 205 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ⊆ 𝐴 → (𝐶 ∩ 𝐴) = 𝐶) |
26 | 23, 25 | syl5eqr 2658 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ⊆ 𝐴 → (𝐴 ∩ 𝐶) = 𝐶) |
27 | 26 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (𝐴 ∩ 𝐶) = 𝐶) |
28 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → 𝐶 ≠ ∅) |
29 | 27, 28 | eqnetrd 2849 |
. . . . . . . . . . . 12
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (𝐴 ∩ 𝐶) ≠ ∅) |
30 | | df-ne 2782 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∩ 𝐶) ≠ ∅ ↔ ¬ (𝐴 ∩ 𝐶) = ∅) |
31 | 30 | biimpi 205 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∩ 𝐶) ≠ ∅ → ¬ (𝐴 ∩ 𝐶) = ∅) |
32 | | iffalse 4045 |
. . . . . . . . . . . 12
⊢ (¬
(𝐴 ∩ 𝐶) = ∅ → if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) = 𝐵) |
33 | 29, 31, 32 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) = 𝐵) |
34 | 22, 33 | syl5eq 2656 |
. . . . . . . . . 10
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝐴 × 𝐵) “ 𝐶) = 𝐵) |
35 | 34 | difeq1d 3689 |
. . . . . . . . 9
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵) = (𝐵 ∖ 𝐵)) |
36 | | difid 3902 |
. . . . . . . . 9
⊢ (𝐵 ∖ 𝐵) = ∅ |
37 | 35, 36 | syl6eq 2660 |
. . . . . . . 8
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵) = ∅) |
38 | 21, 37 | syl5sseq 3616 |
. . . . . . 7
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ ∅) |
39 | | ss0 3926 |
. . . . . . 7
⊢ ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ ∅ → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ∅) |
40 | 38, 39 | syl 17 |
. . . . . 6
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ∅) |
41 | | df-ima 5051 |
. . . . . . . . . . 11
⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶) |
42 | | df-res 5050 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶) = ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) |
43 | 42 | rneqi 5273 |
. . . . . . . . . . 11
⊢ ran
((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) |
44 | 41, 43 | eqtri 2632 |
. . . . . . . . . 10
⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) |
45 | 44 | ineq1i 3772 |
. . . . . . . . 9
⊢ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵) |
46 | | xpss1 5151 |
. . . . . . . . . . . 12
⊢ (𝐶 ⊆ 𝐴 → (𝐶 × V) ⊆ (𝐴 × V)) |
47 | | sslin 3801 |
. . . . . . . . . . . 12
⊢ ((𝐶 × V) ⊆ (𝐴 × V) → ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V))) |
48 | | rnss 5275 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V))) |
49 | 46, 47, 48 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝐶 ⊆ 𝐴 → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V))) |
50 | 49 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V))) |
51 | | ssn0 3928 |
. . . . . . . . . . . 12
⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅) → 𝐴 ≠ ∅) |
52 | 51 | ancoms 468 |
. . . . . . . . . . 11
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → 𝐴 ≠ ∅) |
53 | | inss1 3795 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 × V) ∩ 𝑅) ⊆ (𝐴 × V) |
54 | | ssdif 3707 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 × V) ∩ 𝑅) ⊆ (𝐴 × V) → (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵)) ⊆ ((𝐴 × V) ∖ (𝐴 × 𝐵))) |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵)) ⊆ ((𝐴 × V) ∖ (𝐴 × 𝐵)) |
56 | | incom 3767 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 × V) ∩ (𝑅 ∖ (𝐴 × 𝐵))) = ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) |
57 | | indif2 3829 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 × V) ∩ (𝑅 ∖ (𝐴 × 𝐵))) = (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵)) |
58 | 56, 57 | eqtr3i 2634 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) = (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵)) |
59 | | difxp2 5479 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 × (V ∖ 𝐵)) = ((𝐴 × V) ∖ (𝐴 × 𝐵)) |
60 | 55, 58, 59 | 3sstr4i 3607 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (𝐴 × (V ∖ 𝐵)) |
61 | | rnss 5275 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (𝐴 × (V ∖ 𝐵)) → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ ran (𝐴 × (V ∖ 𝐵))) |
62 | 60, 61 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝐴 ≠ ∅ → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ ran (𝐴 × (V ∖ 𝐵))) |
63 | | rnxp 5483 |
. . . . . . . . . . . . 13
⊢ (𝐴 ≠ ∅ → ran (𝐴 × (V ∖ 𝐵)) = (V ∖ 𝐵)) |
64 | 62, 63 | sseqtrd 3604 |
. . . . . . . . . . . 12
⊢ (𝐴 ≠ ∅ → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (V ∖ 𝐵)) |
65 | | disj2 3976 |
. . . . . . . . . . . 12
⊢ ((ran
((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅ ↔ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (V ∖ 𝐵)) |
66 | 64, 65 | sylibr 223 |
. . . . . . . . . . 11
⊢ (𝐴 ≠ ∅ → (ran
((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅) |
67 | 52, 66 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅) |
68 | | ssdisj 3978 |
. . . . . . . . . 10
⊢ ((ran
((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∧ (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵) = ∅) |
69 | 50, 67, 68 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵) = ∅) |
70 | 45, 69 | syl5eq 2656 |
. . . . . . . 8
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = ∅) |
71 | | disj3 3973 |
. . . . . . . 8
⊢ ((((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = ∅ ↔ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵)) |
72 | 70, 71 | sylib 207 |
. . . . . . 7
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵)) |
73 | 72 | eqcomd 2616 |
. . . . . 6
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) |
74 | 40, 73 | uneq12d 3730 |
. . . . 5
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵)) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))) |
75 | 17, 74 | syl5eq 2656 |
. . . 4
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝑅 “ 𝐶) ∖ 𝐵) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))) |
76 | | uncom 3719 |
. . . . 5
⊢ (∅
∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∪ ∅) |
77 | | un0 3919 |
. . . . 5
⊢ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∪ ∅) = ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) |
78 | 76, 77 | eqtr2i 2633 |
. . . 4
⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) |
79 | 75, 78 | syl6reqr 2663 |
. . 3
⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵)) |
80 | 79 | ancoms 468 |
. 2
⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵)) |
81 | 10, 80 | pm2.61dane 2869 |
1
⊢ (𝐶 ⊆ 𝐴 → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵)) |