Theorem imadifxp 30364

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

Assertion

Ref	Expression
imadifxp	⊢ (𝐶 ⊆ 𝐴 → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))

Proof of Theorem imadifxp

Step	Hyp	Ref	Expression
1		ima0 5912	. . . 4 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ ∅) = ∅
2		imaeq2 5892	. . . 4 ⊢ (𝐶 = ∅ → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 ∖ (𝐴 × 𝐵)) “ ∅))
3		imaeq2 5892	. . . . . . 7 ⊢ (𝐶 = ∅ → (𝑅 “ 𝐶) = (𝑅 “ ∅))
4		ima0 5912	. . . . . . 7 ⊢ (𝑅 “ ∅) = ∅
5	3, 4	eqtrdi 2849	. . . . . 6 ⊢ (𝐶 = ∅ → (𝑅 “ 𝐶) = ∅)
6	5	difeq1d 4049	. . . . 5 ⊢ (𝐶 = ∅ → ((𝑅 “ 𝐶) ∖ 𝐵) = (∅ ∖ 𝐵))
7		0dif 4309	. . . . 5 ⊢ (∅ ∖ 𝐵) = ∅
8	6, 7	eqtrdi 2849	. . . 4 ⊢ (𝐶 = ∅ → ((𝑅 “ 𝐶) ∖ 𝐵) = ∅)
9	1, 2, 8	3eqtr4a 2859	. . 3 ⊢ (𝐶 = ∅ → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))
10	9	adantl 485	. 2 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐶 = ∅) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))
11		uncom 4080	. . . . 5 ⊢ (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∪ ∅)
12		un0 4298	. . . . 5 ⊢ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∪ ∅) = ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)
13	11, 12	eqtr2i 2822	. . . 4 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))
14		inundif 4385	. . . . . . . . 9 ⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) = 𝑅
15	14	imaeq1i 5893	. . . . . . . 8 ⊢ (((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) “ 𝐶) = (𝑅 “ 𝐶)
16		imaundir 5976	. . . . . . . 8 ⊢ (((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) “ 𝐶) = (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))
17	15, 16	eqtr3i 2823	. . . . . . 7 ⊢ (𝑅 “ 𝐶) = (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))
18	17	difeq1i 4046	. . . . . 6 ⊢ ((𝑅 “ 𝐶) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) ∖ 𝐵)
19		difundir 4207	. . . . . 6 ⊢ ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵))
20	18, 19	eqtri 2821	. . . . 5 ⊢ ((𝑅 “ 𝐶) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵))
21		inss2 4156	. . . . . . . . 9 ⊢ (𝑅 ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵)
22		imass1 5931	. . . . . . . . 9 ⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵) → ((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ⊆ ((𝐴 × 𝐵) “ 𝐶))
23		ssdif 4067	. . . . . . . . 9 ⊢ (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ⊆ ((𝐴 × 𝐵) “ 𝐶) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵))
24	21, 22, 23	mp2b 10	. . . . . . . 8 ⊢ (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵)
25		xpima 6006	. . . . . . . . . . 11 ⊢ ((𝐴 × 𝐵) “ 𝐶) = if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵)
26		incom 4128	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶)
27		df-ss 3898	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ⊆ 𝐴 ↔ (𝐶 ∩ 𝐴) = 𝐶)
28	27	biimpi 219	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ⊆ 𝐴 → (𝐶 ∩ 𝐴) = 𝐶)
29	26, 28	syl5eqr 2847	. . . . . . . . . . . . . 14 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ∩ 𝐶) = 𝐶)
30	29	adantl 485	. . . . . . . . . . . . 13 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (𝐴 ∩ 𝐶) = 𝐶)
31		simpl 486	. . . . . . . . . . . . 13 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → 𝐶 ≠ ∅)
32	30, 31	eqnetrd 3054	. . . . . . . . . . . 12 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (𝐴 ∩ 𝐶) ≠ ∅)
33		neneq 2993	. . . . . . . . . . . 12 ⊢ ((𝐴 ∩ 𝐶) ≠ ∅ → ¬ (𝐴 ∩ 𝐶) = ∅)
34		iffalse 4434	. . . . . . . . . . . 12 ⊢ (¬ (𝐴 ∩ 𝐶) = ∅ → if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) = 𝐵)
35	32, 33, 34	3syl 18	. . . . . . . . . . 11 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) = 𝐵)
36	25, 35	syl5eq 2845	. . . . . . . . . 10 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝐴 × 𝐵) “ 𝐶) = 𝐵)
37	36	difeq1d 4049	. . . . . . . . 9 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵) = (𝐵 ∖ 𝐵))
38		difid 4284	. . . . . . . . 9 ⊢ (𝐵 ∖ 𝐵) = ∅
39	37, 38	eqtrdi 2849	. . . . . . . 8 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵) = ∅)
40	24, 39	sseqtrid 3967	. . . . . . 7 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ ∅)
41		ss0 4306	. . . . . . 7 ⊢ ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ ∅ → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ∅)
42	40, 41	syl 17	. . . . . 6 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ∅)
43		df-ima 5532	. . . . . . . . . . 11 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶)
44		df-res 5531	. . . . . . . . . . . 12 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶) = ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V))
45	44	rneqi 5771	. . . . . . . . . . 11 ⊢ ran ((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V))
46	43, 45	eqtri 2821	. . . . . . . . . 10 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V))
47	46	ineq1i 4135	. . . . . . . . 9 ⊢ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵)
48		xpss1 5538	. . . . . . . . . . 11 ⊢ (𝐶 ⊆ 𝐴 → (𝐶 × V) ⊆ (𝐴 × V))
49		sslin 4161	. . . . . . . . . . 11 ⊢ ((𝐶 × V) ⊆ (𝐴 × V) → ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)))
50		rnss 5773	. . . . . . . . . . 11 ⊢ (((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)))
51	48, 49, 50	3syl 18	. . . . . . . . . 10 ⊢ (𝐶 ⊆ 𝐴 → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)))
52		ssn0 4308	. . . . . . . . . . . 12 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅) → 𝐴 ≠ ∅)
53	52	ancoms 462	. . . . . . . . . . 11 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → 𝐴 ≠ ∅)
54		inss1 4155	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 × V) ∩ 𝑅) ⊆ (𝐴 × V)
55		ssdif 4067	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 × V) ∩ 𝑅) ⊆ (𝐴 × V) → (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵)) ⊆ ((𝐴 × V) ∖ (𝐴 × 𝐵)))
56	54, 55	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵)) ⊆ ((𝐴 × V) ∖ (𝐴 × 𝐵))
57		incom 4128	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 × V) ∩ (𝑅 ∖ (𝐴 × 𝐵))) = ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V))
58		indif2 4197	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 × V) ∩ (𝑅 ∖ (𝐴 × 𝐵))) = (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵))
59	57, 58	eqtr3i 2823	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) = (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵))
60		difxp2 5990	. . . . . . . . . . . . . . 15 ⊢ (𝐴 × (V ∖ 𝐵)) = ((𝐴 × V) ∖ (𝐴 × 𝐵))
61	56, 59, 60	3sstr4i 3958	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (𝐴 × (V ∖ 𝐵))
62		rnss 5773	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (𝐴 × (V ∖ 𝐵)) → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ ran (𝐴 × (V ∖ 𝐵)))
63	61, 62	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝐴 ≠ ∅ → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ ran (𝐴 × (V ∖ 𝐵)))
64		rnxp 5994	. . . . . . . . . . . . 13 ⊢ (𝐴 ≠ ∅ → ran (𝐴 × (V ∖ 𝐵)) = (V ∖ 𝐵))
65	63, 64	sseqtrd 3955	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ ∅ → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (V ∖ 𝐵))
66		disj2 4365	. . . . . . . . . . . 12 ⊢ ((ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅ ↔ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (V ∖ 𝐵))
67	65, 66	sylibr 237	. . . . . . . . . . 11 ⊢ (𝐴 ≠ ∅ → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅)
68	53, 67	syl 17	. . . . . . . . . 10 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅)
69		ssdisj 4367	. . . . . . . . . 10 ⊢ ((ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∧ (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵) = ∅)
70	51, 68, 69	syl2an2 685	. . . . . . . . 9 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵) = ∅)
71	47, 70	syl5eq 2845	. . . . . . . 8 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = ∅)
72		disj3 4361	. . . . . . . 8 ⊢ ((((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = ∅ ↔ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵))
73	71, 72	sylib 221	. . . . . . 7 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵))
74	73	eqcomd 2804	. . . . . 6 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))
75	42, 74	uneq12d 4091	. . . . 5 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵)) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)))
76	20, 75	syl5eq 2845	. . . 4 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝑅 “ 𝐶) ∖ 𝐵) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)))
77	13, 76	eqtr4id 2852	. . 3 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))
78	77	ancoms 462	. 2 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))
79	10, 78	pm2.61dane 3074	1 ⊢ (𝐶 ⊆ 𝐴 → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1538   ≠ wne 2987  Vcvv 3441   ∖ cdif 3878   ∪ cun 3879   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  ifcif 4425   × cxp 5517  ran crn 5520   ↾ cres 5521   “ cima 5522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-xp 5525  df-rel 5526  df-cnv 5527  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532

This theorem is referenced by: (None)