Theorem imadifxp 30940

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 5985	. . . 4 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ ∅) = ∅
2		imaeq2 5965	. . . 4 ⊢ (𝐶 = ∅ → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 ∖ (𝐴 × 𝐵)) “ ∅))
3		imaeq2 5965	. . . . . . 7 ⊢ (𝐶 = ∅ → (𝑅 “ 𝐶) = (𝑅 “ ∅))
4		ima0 5985	. . . . . . 7 ⊢ (𝑅 “ ∅) = ∅
5	3, 4	eqtrdi 2794	. . . . . 6 ⊢ (𝐶 = ∅ → (𝑅 “ 𝐶) = ∅)
6	5	difeq1d 4056	. . . . 5 ⊢ (𝐶 = ∅ → ((𝑅 “ 𝐶) ∖ 𝐵) = (∅ ∖ 𝐵))
7		0dif 4335	. . . . 5 ⊢ (∅ ∖ 𝐵) = ∅
8	6, 7	eqtrdi 2794	. . . 4 ⊢ (𝐶 = ∅ → ((𝑅 “ 𝐶) ∖ 𝐵) = ∅)
9	1, 2, 8	3eqtr4a 2804	. . 3 ⊢ (𝐶 = ∅ → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))
10	9	adantl 482	. 2 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐶 = ∅) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))
11		uncom 4087	. . . . 5 ⊢ (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∪ ∅)
12		un0 4324	. . . . 5 ⊢ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∪ ∅) = ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)
13	11, 12	eqtr2i 2767	. . . 4 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))
14		inundif 4412	. . . . . . . . 9 ⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) = 𝑅
15	14	imaeq1i 5966	. . . . . . . 8 ⊢ (((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) “ 𝐶) = (𝑅 “ 𝐶)
16		imaundir 6054	. . . . . . . 8 ⊢ (((𝑅 ∩ (𝐴 × 𝐵)) ∪ (𝑅 ∖ (𝐴 × 𝐵))) “ 𝐶) = (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))
17	15, 16	eqtr3i 2768	. . . . . . 7 ⊢ (𝑅 “ 𝐶) = (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))
18	17	difeq1i 4053	. . . . . 6 ⊢ ((𝑅 “ 𝐶) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) ∖ 𝐵)
19		difundir 4214	. . . . . 6 ⊢ ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵))
20	18, 19	eqtri 2766	. . . . 5 ⊢ ((𝑅 “ 𝐶) ∖ 𝐵) = ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵))
21		inss2 4163	. . . . . . . . 9 ⊢ (𝑅 ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵)
22		imass1 6009	. . . . . . . . 9 ⊢ ((𝑅 ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵) → ((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ⊆ ((𝐴 × 𝐵) “ 𝐶))
23		ssdif 4074	. . . . . . . . 9 ⊢ (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ⊆ ((𝐴 × 𝐵) “ 𝐶) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵))
24	21, 22, 23	mp2b 10	. . . . . . . 8 ⊢ (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵)
25		xpima 6085	. . . . . . . . . . 11 ⊢ ((𝐴 × 𝐵) “ 𝐶) = if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵)
26		incom 4135	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶)
27		df-ss 3904	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ⊆ 𝐴 ↔ (𝐶 ∩ 𝐴) = 𝐶)
28	27	biimpi 215	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ⊆ 𝐴 → (𝐶 ∩ 𝐴) = 𝐶)
29	26, 28	eqtr3id 2792	. . . . . . . . . . . . . 14 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ∩ 𝐶) = 𝐶)
30	29	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (𝐴 ∩ 𝐶) = 𝐶)
31		simpl 483	. . . . . . . . . . . . 13 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → 𝐶 ≠ ∅)
32	30, 31	eqnetrd 3011	. . . . . . . . . . . 12 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (𝐴 ∩ 𝐶) ≠ ∅)
33		neneq 2949	. . . . . . . . . . . 12 ⊢ ((𝐴 ∩ 𝐶) ≠ ∅ → ¬ (𝐴 ∩ 𝐶) = ∅)
34		iffalse 4468	. . . . . . . . . . . 12 ⊢ (¬ (𝐴 ∩ 𝐶) = ∅ → if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) = 𝐵)
35	32, 33, 34	3syl 18	. . . . . . . . . . 11 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) = 𝐵)
36	25, 35	eqtrid 2790	. . . . . . . . . 10 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝐴 × 𝐵) “ 𝐶) = 𝐵)
37	36	difeq1d 4056	. . . . . . . . 9 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵) = (𝐵 ∖ 𝐵))
38		difid 4304	. . . . . . . . 9 ⊢ (𝐵 ∖ 𝐵) = ∅
39	37, 38	eqtrdi 2794	. . . . . . . 8 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝐴 × 𝐵) “ 𝐶) ∖ 𝐵) = ∅)
40	24, 39	sseqtrid 3973	. . . . . . 7 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ ∅)
41		ss0 4332	. . . . . . 7 ⊢ ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ⊆ ∅ → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ∅)
42	40, 41	syl 17	. . . . . 6 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ∅)
43		df-ima 5602	. . . . . . . . . . 11 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶)
44		df-res 5601	. . . . . . . . . . . 12 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶) = ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V))
45	44	rneqi 5846	. . . . . . . . . . 11 ⊢ ran ((𝑅 ∖ (𝐴 × 𝐵)) ↾ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V))
46	43, 45	eqtri 2766	. . . . . . . . . 10 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V))
47	46	ineq1i 4142	. . . . . . . . 9 ⊢ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵)
48		xpss1 5608	. . . . . . . . . . 11 ⊢ (𝐶 ⊆ 𝐴 → (𝐶 × V) ⊆ (𝐴 × V))
49		sslin 4168	. . . . . . . . . . 11 ⊢ ((𝐶 × V) ⊆ (𝐴 × V) → ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)))
50		rnss 5848	. . . . . . . . . . 11 ⊢ (((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)))
51	48, 49, 50	3syl 18	. . . . . . . . . 10 ⊢ (𝐶 ⊆ 𝐴 → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)))
52		ssn0 4334	. . . . . . . . . . . 12 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅) → 𝐴 ≠ ∅)
53	52	ancoms 459	. . . . . . . . . . 11 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → 𝐴 ≠ ∅)
54		inss1 4162	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 × V) ∩ 𝑅) ⊆ (𝐴 × V)
55		ssdif 4074	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 × V) ∩ 𝑅) ⊆ (𝐴 × V) → (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵)) ⊆ ((𝐴 × V) ∖ (𝐴 × 𝐵)))
56	54, 55	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵)) ⊆ ((𝐴 × V) ∖ (𝐴 × 𝐵))
57		incom 4135	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 × V) ∩ (𝑅 ∖ (𝐴 × 𝐵))) = ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V))
58		indif2 4204	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 × V) ∩ (𝑅 ∖ (𝐴 × 𝐵))) = (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵))
59	57, 58	eqtr3i 2768	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) = (((𝐴 × V) ∩ 𝑅) ∖ (𝐴 × 𝐵))
60		difxp2 6069	. . . . . . . . . . . . . . 15 ⊢ (𝐴 × (V ∖ 𝐵)) = ((𝐴 × V) ∖ (𝐴 × 𝐵))
61	56, 59, 60	3sstr4i 3964	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (𝐴 × (V ∖ 𝐵))
62		rnss 5848	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (𝐴 × (V ∖ 𝐵)) → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ ran (𝐴 × (V ∖ 𝐵)))
63	61, 62	mp1i 13	. . . . . . . . . . . . 13 ⊢ (𝐴 ≠ ∅ → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ ran (𝐴 × (V ∖ 𝐵)))
64		rnxp 6073	. . . . . . . . . . . . 13 ⊢ (𝐴 ≠ ∅ → ran (𝐴 × (V ∖ 𝐵)) = (V ∖ 𝐵))
65	63, 64	sseqtrd 3961	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ ∅ → ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (V ∖ 𝐵))
66		disj2 4391	. . . . . . . . . . . 12 ⊢ ((ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅ ↔ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ⊆ (V ∖ 𝐵))
67	65, 66	sylibr 233	. . . . . . . . . . 11 ⊢ (𝐴 ≠ ∅ → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅)
68	53, 67	syl 17	. . . . . . . . . 10 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅)
69		ssdisj 4393	. . . . . . . . . 10 ⊢ ((ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ⊆ ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∧ (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐴 × V)) ∩ 𝐵) = ∅) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵) = ∅)
70	51, 68, 69	syl2an2 683	. . . . . . . . 9 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (ran ((𝑅 ∖ (𝐴 × 𝐵)) ∩ (𝐶 × V)) ∩ 𝐵) = ∅)
71	47, 70	eqtrid 2790	. . . . . . . 8 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = ∅)
72		disj3 4387	. . . . . . . 8 ⊢ ((((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∩ 𝐵) = ∅ ↔ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵))
73	71, 72	sylib 217	. . . . . . 7 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵))
74	73	eqcomd 2744	. . . . . 6 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) = ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶))
75	42, 74	uneq12d 4098	. . . . 5 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((((𝑅 ∩ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵) ∪ (((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) ∖ 𝐵)) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)))
76	20, 75	eqtrid 2790	. . . 4 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝑅 “ 𝐶) ∖ 𝐵) = (∅ ∪ ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶)))
77	13, 76	eqtr4id 2797	. . 3 ⊢ ((𝐶 ≠ ∅ ∧ 𝐶 ⊆ 𝐴) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))
78	77	ancoms 459	. 2 ⊢ ((𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅) → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))
79	10, 78	pm2.61dane 3032	1 ⊢ (𝐶 ⊆ 𝐴 → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1539   ≠ wne 2943  Vcvv 3432   ∖ cdif 3884   ∪ cun 3885   ∩ cin 3886   ⊆ wss 3887  ∅c0 4256  ifcif 4459   × cxp 5587  ran crn 5590   ↾ cres 5591   “ cima 5592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-xp 5595  df-rel 5596  df-cnv 5597  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602

This theorem is referenced by: (None)