Theorem imadifxp 32100

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 6076	. . . 4 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ ∅) = ∅
2		imaeq2 6055	. . . 4 ⊢ (𝐶 = ∅ → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 ∖ (𝐴 × 𝐵)) “ ∅))
3		imaeq2 6055	. . . . . . 7 ⊢ (𝐶 = ∅ → (𝑅 “ 𝐶) = (𝑅 “ ∅))
4		ima0 6076	. . . . . . 7 ⊢ (𝑅 “ ∅) = ∅
5	3, 4	eqtrdi 2787	. . . . . 6 ⊢ (𝐶 = ∅ → (𝑅 “ 𝐶) = ∅)
6	5	difeq1d 4121	. . . . 5 ⊢ (𝐶 = ∅ → ((𝑅 “ 𝐶) ∖ 𝐵) = (∅ ∖ 𝐵))
7		0dif 4401	. . . . 5 ⊢ (∅ ∖ 𝐵) = ∅
8	6, 7	eqtrdi 2787	. . . 4 ⊢ (𝐶 = ∅ → ((𝑅 “ 𝐶) ∖ 𝐵) = ∅)
9	1, 2, 8	3eqtr4a 2797	. . 3 ⊢ (𝐶 = ∅ → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))
10	9	adantl 481	. 2 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐶 = ∅) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))
11		uncom 4153	. . . . 5 ⊢ (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∪ ∅)
12		un0 4390	. . . . 5 ⊢ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∪ ∅) = ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)
13	11, 12	eqtr2i 2760	. . . 4 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))
14		inundif 4478	. . . . . . . . 9 ⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) = 𝑅
15	14	imaeq1i 6056	. . . . . . . 8 ⊢ (((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) “ 𝐶) = (𝑅 “ 𝐶)
16		imaundir 6150	. . . . . . . 8 ⊢ (((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) “ 𝐶) = (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))
17	15, 16	eqtr3i 2761	. . . . . . 7 ⊢ (𝑅 “ 𝐶) = (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))
18	17	difeq1i 4118	. . . . . 6 ⊢ ((𝑅 “ 𝐶) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) ∖ 𝐵)
19		difundir 4280	. . . . . 6 ⊢ ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵))
20	18, 19	eqtri 2759	. . . . 5 ⊢ ((𝑅 “ 𝐶) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵))
21		inss2 4229	. . . . . . . . 9 ⊢ (𝑅 ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵)
22		imass1 6100	. . . . . . . . 9 ⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵) → ((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ⊆ ((𝐴 × 𝐵) “ 𝐶))
23		ssdif 4139	. . . . . . . . 9 ⊢ (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ⊆ ((𝐴 × 𝐵) “ 𝐶) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵))
24	21, 22, 23	mp2b 10	. . . . . . . 8 ⊢ (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵)
25		xpima 6181	. . . . . . . . . . 11 ⊢ ((𝐴 × 𝐵) “ 𝐶) = if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵)
26		incom 4201	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶)
27		df-ss 3965	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ⊆ 𝐴 ↔ (𝐶 ∩ 𝐴) = 𝐶)
28	27	biimpi 215	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ⊆ 𝐴 → (𝐶 ∩ 𝐴) = 𝐶)
29	26, 28	eqtr3id 2785	. . . . . . . . . . . . . 14 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ∩ 𝐶) = 𝐶)
30	29	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (𝐴 ∩ 𝐶) = 𝐶)
31		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → 𝐶 ≠ ∅)
32	30, 31	eqnetrd 3007	. . . . . . . . . . . 12 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (𝐴 ∩ 𝐶) ≠ ∅)
33		neneq 2945	. . . . . . . . . . . 12 ⊢ ((𝐴 ∩ 𝐶) ≠ ∅ → ¬ (𝐴 ∩ 𝐶) = ∅)
34		iffalse 4537	. . . . . . . . . . . 12 ⊢ (¬ (𝐴 ∩ 𝐶) = ∅ → if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) = 𝐵)
35	32, 33, 34	3syl 18	. . . . . . . . . . 11 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) = 𝐵)
36	25, 35	eqtrid 2783	. . . . . . . . . 10 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝐴 × 𝐵) “ 𝐶) = 𝐵)
37	36	difeq1d 4121	. . . . . . . . 9 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵) = (𝐵 ∖ 𝐵))
38		difid 4370	. . . . . . . . 9 ⊢ (𝐵 ∖ 𝐵) = ∅
39	37, 38	eqtrdi 2787	. . . . . . . 8 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵) = ∅)
40	24, 39	sseqtrid 4034	. . . . . . 7 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ ∅)
41		ss0 4398	. . . . . . 7 ⊢ ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ ∅ → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ∅)
42	40, 41	syl 17	. . . . . 6 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ∅)
43		df-ima 5689	. . . . . . . . . . 11 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶)
44		df-res 5688	. . . . . . . . . . . 12 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶) = ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V))
45	44	rneqi 5936	. . . . . . . . . . 11 ⊢ ran ((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V))
46	43, 45	eqtri 2759	. . . . . . . . . 10 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V))
47	46	ineq1i 4208	. . . . . . . . 9 ⊢ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵)
48		xpss1 5695	. . . . . . . . . . 11 ⊢ (𝐶 ⊆ 𝐴 → (𝐶 × V) ⊆ (𝐴 × V))
49		sslin 4234	. . . . . . . . . . 11 ⊢ ((𝐶 × V) ⊆ (𝐴 × V) → ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)))
50		rnss 5938	. . . . . . . . . . 11 ⊢ (((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)))
51	48, 49, 50	3syl 18	. . . . . . . . . 10 ⊢ (𝐶 ⊆ 𝐴 → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)))
52		ssn0 4400	. . . . . . . . . . . 12 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅) → 𝐴 ≠ ∅)
53	52	ancoms 458	. . . . . . . . . . 11 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → 𝐴 ≠ ∅)
54		inss1 4228	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 × V) ∩ 𝑅) ⊆ (𝐴 × V)
55		ssdif 4139	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 × V) ∩ 𝑅) ⊆ (𝐴 × V) → (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵)) ⊆ ((𝐴 × V) ∖ (𝐴 × 𝐵)))
56	54, 55	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵)) ⊆ ((𝐴 × V) ∖ (𝐴 × 𝐵))
57		incom 4201	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 × V) ∩ (𝑅 ∖ (𝐴 × 𝐵))) = ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V))
58		indif2 4270	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 × V) ∩ (𝑅 ∖ (𝐴 × 𝐵))) = (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵))
59	57, 58	eqtr3i 2761	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) = (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵))
60		difxp2 6165	. . . . . . . . . . . . . . 15 ⊢ (𝐴 × (V ∖ 𝐵)) = ((𝐴 × V) ∖ (𝐴 × 𝐵))
61	56, 59, 60	3sstr4i 4025	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (𝐴 × (V ∖ 𝐵))
62		rnss 5938	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (𝐴 × (V ∖ 𝐵)) → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ ran (𝐴 × (V ∖ 𝐵)))
63	61, 62	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝐴 ≠ ∅ → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ ran (𝐴 × (V ∖ 𝐵)))
64		rnxp 6169	. . . . . . . . . . . . 13 ⊢ (𝐴 ≠ ∅ → ran (𝐴 × (V ∖ 𝐵)) = (V ∖ 𝐵))
65	63, 64	sseqtrd 4022	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ ∅ → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (V ∖ 𝐵))
66		disj2 4457	. . . . . . . . . . . 12 ⊢ ((ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅ ↔ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (V ∖ 𝐵))
67	65, 66	sylibr 233	. . . . . . . . . . 11 ⊢ (𝐴 ≠ ∅ → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅)
68	53, 67	syl 17	. . . . . . . . . 10 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅)
69		ssdisj 4459	. . . . . . . . . 10 ⊢ ((ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∧ (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵) = ∅)
70	51, 68, 69	syl2an2 683	. . . . . . . . 9 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵) = ∅)
71	47, 70	eqtrid 2783	. . . . . . . 8 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = ∅)
72		disj3 4453	. . . . . . . 8 ⊢ ((((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = ∅ ↔ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵))
73	71, 72	sylib 217	. . . . . . 7 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵))
74	73	eqcomd 2737	. . . . . 6 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))
75	42, 74	uneq12d 4164	. . . . 5 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵)) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)))
76	20, 75	eqtrid 2783	. . . 4 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝑅 “ 𝐶) ∖ 𝐵) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)))
77	13, 76	eqtr4id 2790	. . 3 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))
78	77	ancoms 458	. 2 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))
79	10, 78	pm2.61dane 3028	1 ⊢ (𝐶 ⊆ 𝐴 → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ≠ wne 2939  Vcvv 3473   ∖ cdif 3945   ∪ cun 3946   ∩ cin 3947   ⊆ wss 3948  ∅c0 4322  ifcif 4528   × cxp 5674  ran crn 5677   ↾ cres 5678   “ cima 5679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-xp 5682  df-rel 5683  df-cnv 5684  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689

This theorem is referenced by: (None)