imadifxp

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

		Ref	Expression
	Assertion	imadifxp	$⊢ C \subseteq A \to (R ∖ (A \times B)) [C] = R [C] ∖ B$

Proof

Step	Hyp	Ref	Expression
1		ima0	$⊢ (R ∖ (A \times B)) [\emptyset] = \emptyset$
2		imaeq2	$⊢ C = \emptyset \to (R ∖ (A \times B)) [C] = (R ∖ (A \times B)) [\emptyset]$
3		imaeq2	$⊢ C = \emptyset \to R [C] = R [\emptyset]$
4		ima0	$⊢ R [\emptyset] = \emptyset$
5	3 4	eqtrdi	$⊢ C = \emptyset \to R [C] = \emptyset$
6	5	difeq1d	$⊢ C = \emptyset \to R [C] ∖ B = \emptyset ∖ B$
7		0dif	$⊢ \emptyset ∖ B = \emptyset$
8	6 7	eqtrdi	$⊢ C = \emptyset \to R [C] ∖ B = \emptyset$
9	1 2 8	3eqtr4a	$⊢ C = \emptyset \to (R ∖ (A \times B)) [C] = R [C] ∖ B$
10	9	adantl	$⊢ (C \subseteq A \land C = \emptyset) \to (R ∖ (A \times B)) [C] = R [C] ∖ B$
11		uncom	$⊢ \emptyset \cup (R ∖ (A \times B)) [C] = (R ∖ (A \times B)) [C] \cup \emptyset$
12		un0	$⊢ (R ∖ (A \times B)) [C] \cup \emptyset = (R ∖ (A \times B)) [C]$
13	11 12	eqtr2i	$⊢ (R ∖ (A \times B)) [C] = \emptyset \cup (R ∖ (A \times B)) [C]$
14		inundif	$⊢ (R \cap (A \times B)) \cup (R ∖ (A \times B)) = R$
15	14	imaeq1i	$⊢ ((R \cap (A \times B)) \cup (R ∖ (A \times B))) [C] = R [C]$
16		imaundir	$⊢ ((R \cap (A \times B)) \cup (R ∖ (A \times B))) [C] = (R \cap (A \times B)) [C] \cup (R ∖ (A \times B)) [C]$
17	15 16	eqtr3i	$⊢ R [C] = (R \cap (A \times B)) [C] \cup (R ∖ (A \times B)) [C]$
18	17	difeq1i	$⊢ R [C] ∖ B = ((R \cap (A \times B)) [C] \cup (R ∖ (A \times B)) [C]) ∖ B$
19		difundir	$⊢ ((R \cap (A \times B)) [C] \cup (R ∖ (A \times B)) [C]) ∖ B = ((R \cap (A \times B)) [C] ∖ B) \cup ((R ∖ (A \times B)) [C] ∖ B)$
20	18 19	eqtri	$⊢ R [C] ∖ B = ((R \cap (A \times B)) [C] ∖ B) \cup ((R ∖ (A \times B)) [C] ∖ B)$
21		inss2	$⊢ R \cap (A \times B) \subseteq A \times B$
22		imass1	$⊢ R \cap (A \times B) \subseteq A \times B \to (R \cap (A \times B)) [C] \subseteq (A \times B) [C]$
23		ssdif	$⊢ (R \cap (A \times B)) [C] \subseteq (A \times B) [C] \to (R \cap (A \times B)) [C] ∖ B \subseteq (A \times B) [C] ∖ B$
24	21 22 23	mp2b	$⊢ (R \cap (A \times B)) [C] ∖ B \subseteq (A \times B) [C] ∖ B$
25		xpima	$⊢ (A \times B) [C] = if (A \cap C = \emptyset, \emptyset, B)$
26		incom	$⊢ C \cap A = A \cap C$
27		df-ss	$⊢ C \subseteq A \leftrightarrow C \cap A = C$
28	27	biimpi	$⊢ C \subseteq A \to C \cap A = C$
29	26 28	eqtr3id	$⊢ C \subseteq A \to A \cap C = C$
30	29	adantl	$⊢ (C \neq \emptyset \land C \subseteq A) \to A \cap C = C$
31		simpl	$⊢ (C \neq \emptyset \land C \subseteq A) \to C \neq \emptyset$
32	30 31	eqnetrd	$⊢ (C \neq \emptyset \land C \subseteq A) \to A \cap C \neq \emptyset$
33		neneq	$⊢ A \cap C \neq \emptyset \to \neg A \cap C = \emptyset$
34		iffalse	$⊢ \neg A \cap C = \emptyset \to if (A \cap C = \emptyset, \emptyset, B) = B$
35	32 33 34	3syl	$⊢ (C \neq \emptyset \land C \subseteq A) \to if (A \cap C = \emptyset, \emptyset, B) = B$
36	25 35	syl5eq	$⊢ (C \neq \emptyset \land C \subseteq A) \to (A \times B) [C] = B$
37	36	difeq1d	$⊢ (C \neq \emptyset \land C \subseteq A) \to (A \times B) [C] ∖ B = B ∖ B$
38		difid	$⊢ B ∖ B = \emptyset$
39	37 38	eqtrdi	$⊢ (C \neq \emptyset \land C \subseteq A) \to (A \times B) [C] ∖ B = \emptyset$
40	24 39	sseqtrid	$⊢ (C \neq \emptyset \land C \subseteq A) \to (R \cap (A \times B)) [C] ∖ B \subseteq \emptyset$
41		ss0	$⊢ (R \cap (A \times B)) [C] ∖ B \subseteq \emptyset \to (R \cap (A \times B)) [C] ∖ B = \emptyset$
42	40 41	syl	$⊢ (C \neq \emptyset \land C \subseteq A) \to (R \cap (A \times B)) [C] ∖ B = \emptyset$
43		df-ima	$⊢ (R ∖ (A \times B)) [C] = ran ({(R ∖ (A \times B)) ↾}_{C})$
44		df-res	$⊢ {(R ∖ (A \times B)) ↾}_{C} = (R ∖ (A \times B)) \cap (C \times V)$
45	44	rneqi	$⊢ ran ({(R ∖ (A \times B)) ↾}_{C}) = ran ((R ∖ (A \times B)) \cap (C \times V))$
46	43 45	eqtri	$⊢ (R ∖ (A \times B)) [C] = ran ((R ∖ (A \times B)) \cap (C \times V))$
47	46	ineq1i	$⊢ (R ∖ (A \times B)) [C] \cap B = ran ((R ∖ (A \times B)) \cap (C \times V)) \cap B$
48		xpss1	$⊢ C \subseteq A \to C \times V \subseteq A \times V$
49		sslin	$⊢ C \times V \subseteq A \times V \to (R ∖ (A \times B)) \cap (C \times V) \subseteq (R ∖ (A \times B)) \cap (A \times V)$
50		rnss	$⊢ (R ∖ (A \times B)) \cap (C \times V) \subseteq (R ∖ (A \times B)) \cap (A \times V) \to ran ((R ∖ (A \times B)) \cap (C \times V)) \subseteq ran ((R ∖ (A \times B)) \cap (A \times V))$
51	48 49 50	3syl	$⊢ C \subseteq A \to ran ((R ∖ (A \times B)) \cap (C \times V)) \subseteq ran ((R ∖ (A \times B)) \cap (A \times V))$
52		ssn0	$⊢ (C \subseteq A \land C \neq \emptyset) \to A \neq \emptyset$
53	52	ancoms	$⊢ (C \neq \emptyset \land C \subseteq A) \to A \neq \emptyset$
54		inss1	$⊢ (A \times V) \cap R \subseteq A \times V$
55		ssdif	$⊢ (A \times V) \cap R \subseteq A \times V \to ((A \times V) \cap R) ∖ (A \times B) \subseteq (A \times V) ∖ (A \times B)$
56	54 55	ax-mp	$⊢ ((A \times V) \cap R) ∖ (A \times B) \subseteq (A \times V) ∖ (A \times B)$
57		incom	$⊢ (A \times V) \cap (R ∖ (A \times B)) = (R ∖ (A \times B)) \cap (A \times V)$
58		indif2	$⊢ (A \times V) \cap (R ∖ (A \times B)) = ((A \times V) \cap R) ∖ (A \times B)$
59	57 58	eqtr3i	$⊢ (R ∖ (A \times B)) \cap (A \times V) = ((A \times V) \cap R) ∖ (A \times B)$
60		difxp2	$⊢ A \times (V ∖ B) = (A \times V) ∖ (A \times B)$
61	56 59 60	3sstr4i	$⊢ (R ∖ (A \times B)) \cap (A \times V) \subseteq A \times (V ∖ B)$
62		rnss	$⊢ (R ∖ (A \times B)) \cap (A \times V) \subseteq A \times (V ∖ B) \to ran ((R ∖ (A \times B)) \cap (A \times V)) \subseteq ran (A \times (V ∖ B))$
63	61 62	mp1i	$⊢ A \neq \emptyset \to ran ((R ∖ (A \times B)) \cap (A \times V)) \subseteq ran (A \times (V ∖ B))$
64		rnxp	$⊢ A \neq \emptyset \to ran (A \times (V ∖ B)) = V ∖ B$
65	63 64	sseqtrd	$⊢ A \neq \emptyset \to ran ((R ∖ (A \times B)) \cap (A \times V)) \subseteq V ∖ B$
66		disj2	$⊢ ran ((R ∖ (A \times B)) \cap (A \times V)) \cap B = \emptyset \leftrightarrow ran ((R ∖ (A \times B)) \cap (A \times V)) \subseteq V ∖ B$
67	65 66	sylibr	$⊢ A \neq \emptyset \to ran ((R ∖ (A \times B)) \cap (A \times V)) \cap B = \emptyset$
68	53 67	syl	$⊢ (C \neq \emptyset \land C \subseteq A) \to ran ((R ∖ (A \times B)) \cap (A \times V)) \cap B = \emptyset$
69		ssdisj	$⊢ (ran ((R ∖ (A \times B)) \cap (C \times V)) \subseteq ran ((R ∖ (A \times B)) \cap (A \times V)) \land ran ((R ∖ (A \times B)) \cap (A \times V)) \cap B = \emptyset) \to ran ((R ∖ (A \times B)) \cap (C \times V)) \cap B = \emptyset$
70	51 68 69	syl2an2	$⊢ (C \neq \emptyset \land C \subseteq A) \to ran ((R ∖ (A \times B)) \cap (C \times V)) \cap B = \emptyset$
71	47 70	syl5eq	$⊢ (C \neq \emptyset \land C \subseteq A) \to (R ∖ (A \times B)) [C] \cap B = \emptyset$
72		disj3	$⊢ (R ∖ (A \times B)) [C] \cap B = \emptyset \leftrightarrow (R ∖ (A \times B)) [C] = (R ∖ (A \times B)) [C] ∖ B$
73	71 72	sylib	$⊢ (C \neq \emptyset \land C \subseteq A) \to (R ∖ (A \times B)) [C] = (R ∖ (A \times B)) [C] ∖ B$
74	73	eqcomd	$⊢ (C \neq \emptyset \land C \subseteq A) \to (R ∖ (A \times B)) [C] ∖ B = (R ∖ (A \times B)) [C]$
75	42 74	uneq12d	$⊢ (C \neq \emptyset \land C \subseteq A) \to ((R \cap (A \times B)) [C] ∖ B) \cup ((R ∖ (A \times B)) [C] ∖ B) = \emptyset \cup (R ∖ (A \times B)) [C]$
76	20 75	syl5eq	$⊢ (C \neq \emptyset \land C \subseteq A) \to R [C] ∖ B = \emptyset \cup (R ∖ (A \times B)) [C]$
77	13 76	eqtr4id	$⊢ (C \neq \emptyset \land C \subseteq A) \to (R ∖ (A \times B)) [C] = R [C] ∖ B$
78	77	ancoms	$⊢ (C \subseteq A \land C \neq \emptyset) \to (R ∖ (A \times B)) [C] = R [C] ∖ B$
79	10 78	pm2.61dane	$⊢ C \subseteq A \to (R ∖ (A \times B)) [C] = R [C] ∖ B$

Metamath Proof Explorer

Theorem imadifxp

Proof