Theorem imadifxp 32530

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 6048	. . . 4 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ ∅) = ∅
2		imaeq2 6027	. . . 4 ⊢ (𝐶 = ∅ → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 ∖ (𝐴 × 𝐵)) “ ∅))
3		imaeq2 6027	. . . . . . 7 ⊢ (𝐶 = ∅ → (𝑅 “ 𝐶) = (𝑅 “ ∅))
4		ima0 6048	. . . . . . 7 ⊢ (𝑅 “ ∅) = ∅
5	3, 4	eqtrdi 2780	. . . . . 6 ⊢ (𝐶 = ∅ → (𝑅 “ 𝐶) = ∅)
6	5	difeq1d 4088	. . . . 5 ⊢ (𝐶 = ∅ → ((𝑅 “ 𝐶) ∖ 𝐵) = (∅ ∖ 𝐵))
7		0dif 4368	. . . . 5 ⊢ (∅ ∖ 𝐵) = ∅
8	6, 7	eqtrdi 2780	. . . 4 ⊢ (𝐶 = ∅ → ((𝑅 “ 𝐶) ∖ 𝐵) = ∅)
9	1, 2, 8	3eqtr4a 2790	. . 3 ⊢ (𝐶 = ∅ → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))
10	9	adantl 481	. 2 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐶 = ∅) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))
11		uncom 4121	. . . . 5 ⊢ (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∪ ∅)
12		un0 4357	. . . . 5 ⊢ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∪ ∅) = ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)
13	11, 12	eqtr2i 2753	. . . 4 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))
14		inundif 4442	. . . . . . . . 9 ⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) = 𝑅
15	14	imaeq1i 6028	. . . . . . . 8 ⊢ (((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) “ 𝐶) = (𝑅 “ 𝐶)
16		imaundir 6123	. . . . . . . 8 ⊢ (((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) “ 𝐶) = (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))
17	15, 16	eqtr3i 2754	. . . . . . 7 ⊢ (𝑅 “ 𝐶) = (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))
18	17	difeq1i 4085	. . . . . 6 ⊢ ((𝑅 “ 𝐶) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) ∖ 𝐵)
19		difundir 4254	. . . . . 6 ⊢ ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵))
20	18, 19	eqtri 2752	. . . . 5 ⊢ ((𝑅 “ 𝐶) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵))
21		inss2 4201	. . . . . . . . 9 ⊢ (𝑅 ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵)
22		imass1 6072	. . . . . . . . 9 ⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵) → ((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ⊆ ((𝐴 × 𝐵) “ 𝐶))
23		ssdif 4107	. . . . . . . . 9 ⊢ (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ⊆ ((𝐴 × 𝐵) “ 𝐶) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵))
24	21, 22, 23	mp2b 10	. . . . . . . 8 ⊢ (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵)
25		xpima 6155	. . . . . . . . . . 11 ⊢ ((𝐴 × 𝐵) “ 𝐶) = if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵)
26		incom 4172	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶)
27		dfss2 3932	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ⊆ 𝐴 ↔ (𝐶 ∩ 𝐴) = 𝐶)
28	27	biimpi 216	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ⊆ 𝐴 → (𝐶 ∩ 𝐴) = 𝐶)
29	26, 28	eqtr3id 2778	. . . . . . . . . . . . . 14 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ∩ 𝐶) = 𝐶)
30	29	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (𝐴 ∩ 𝐶) = 𝐶)
31		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → 𝐶 ≠ ∅)
32	30, 31	eqnetrd 2992	. . . . . . . . . . . 12 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (𝐴 ∩ 𝐶) ≠ ∅)
33		neneq 2931	. . . . . . . . . . . 12 ⊢ ((𝐴 ∩ 𝐶) ≠ ∅ → ¬ (𝐴 ∩ 𝐶) = ∅)
34		iffalse 4497	. . . . . . . . . . . 12 ⊢ (¬ (𝐴 ∩ 𝐶) = ∅ → if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) = 𝐵)
35	32, 33, 34	3syl 18	. . . . . . . . . . 11 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) = 𝐵)
36	25, 35	eqtrid 2776	. . . . . . . . . 10 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝐴 × 𝐵) “ 𝐶) = 𝐵)
37	36	difeq1d 4088	. . . . . . . . 9 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵) = (𝐵 ∖ 𝐵))
38		difid 4339	. . . . . . . . 9 ⊢ (𝐵 ∖ 𝐵) = ∅
39	37, 38	eqtrdi 2780	. . . . . . . 8 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵) = ∅)
40	24, 39	sseqtrid 3989	. . . . . . 7 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ ∅)
41		ss0 4365	. . . . . . 7 ⊢ ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ ∅ → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ∅)
42	40, 41	syl 17	. . . . . 6 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ∅)
43		df-ima 5651	. . . . . . . . . . 11 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶)
44		df-res 5650	. . . . . . . . . . . 12 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶) = ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V))
45	44	rneqi 5901	. . . . . . . . . . 11 ⊢ ran ((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V))
46	43, 45	eqtri 2752	. . . . . . . . . 10 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V))
47	46	ineq1i 4179	. . . . . . . . 9 ⊢ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵)
48		xpss1 5657	. . . . . . . . . . 11 ⊢ (𝐶 ⊆ 𝐴 → (𝐶 × V) ⊆ (𝐴 × V))
49		sslin 4206	. . . . . . . . . . 11 ⊢ ((𝐶 × V) ⊆ (𝐴 × V) → ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)))
50		rnss 5903	. . . . . . . . . . 11 ⊢ (((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)))
51	48, 49, 50	3syl 18	. . . . . . . . . 10 ⊢ (𝐶 ⊆ 𝐴 → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)))
52		ssn0 4367	. . . . . . . . . . . 12 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅) → 𝐴 ≠ ∅)
53	52	ancoms 458	. . . . . . . . . . 11 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → 𝐴 ≠ ∅)
54		inss1 4200	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 × V) ∩ 𝑅) ⊆ (𝐴 × V)
55		ssdif 4107	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 × V) ∩ 𝑅) ⊆ (𝐴 × V) → (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵)) ⊆ ((𝐴 × V) ∖ (𝐴 × 𝐵)))
56	54, 55	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵)) ⊆ ((𝐴 × V) ∖ (𝐴 × 𝐵))
57		incom 4172	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 × V) ∩ (𝑅 ∖ (𝐴 × 𝐵))) = ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V))
58		indif2 4244	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 × V) ∩ (𝑅 ∖ (𝐴 × 𝐵))) = (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵))
59	57, 58	eqtr3i 2754	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) = (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵))
60		difxp2 6139	. . . . . . . . . . . . . . 15 ⊢ (𝐴 × (V ∖ 𝐵)) = ((𝐴 × V) ∖ (𝐴 × 𝐵))
61	56, 59, 60	3sstr4i 3998	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (𝐴 × (V ∖ 𝐵))
62		rnss 5903	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (𝐴 × (V ∖ 𝐵)) → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ ran (𝐴 × (V ∖ 𝐵)))
63	61, 62	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝐴 ≠ ∅ → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ ran (𝐴 × (V ∖ 𝐵)))
64		rnxp 6143	. . . . . . . . . . . . 13 ⊢ (𝐴 ≠ ∅ → ran (𝐴 × (V ∖ 𝐵)) = (V ∖ 𝐵))
65	63, 64	sseqtrd 3983	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ ∅ → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (V ∖ 𝐵))
66		disj2 4421	. . . . . . . . . . . 12 ⊢ ((ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅ ↔ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (V ∖ 𝐵))
67	65, 66	sylibr 234	. . . . . . . . . . 11 ⊢ (𝐴 ≠ ∅ → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅)
68	53, 67	syl 17	. . . . . . . . . 10 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅)
69		ssdisj 4423	. . . . . . . . . 10 ⊢ ((ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∧ (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵) = ∅)
70	51, 68, 69	syl2an2 686	. . . . . . . . 9 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵) = ∅)
71	47, 70	eqtrid 2776	. . . . . . . 8 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = ∅)
72		disj3 4417	. . . . . . . 8 ⊢ ((((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = ∅ ↔ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵))
73	71, 72	sylib 218	. . . . . . 7 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵))
74	73	eqcomd 2735	. . . . . 6 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))
75	42, 74	uneq12d 4132	. . . . 5 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵)) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)))
76	20, 75	eqtrid 2776	. . . 4 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝑅 “ 𝐶) ∖ 𝐵) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)))
77	13, 76	eqtr4id 2783	. . 3 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))
78	77	ancoms 458	. 2 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))
79	10, 78	pm2.61dane 3012	1 ⊢ (𝐶 ⊆ 𝐴 → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ≠ wne 2925  Vcvv 3447   ∖ cdif 3911   ∪ cun 3912   ∩ cin 3913   ⊆ wss 3914  ∅c0 4296  ifcif 4488   × cxp 5636  ran crn 5639   ↾ cres 5640   “ cima 5641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651

This theorem is referenced by: (None)