mvdco

Description: Composing two permutations moves at most the union of the points. (Contributed by Stefan O'Rear, 22-Aug-2015)

		Ref	Expression
	Assertion	mvdco	$⊢ dom ((F \circ G) ∖ I) \subseteq dom (F ∖ I) \cup dom (G ∖ I)$

Proof

Step	Hyp	Ref	Expression
1		inundif	$⊢ (G \cap I) \cup (G ∖ I) = G$
2	1	coeq2i	$⊢ F \circ ((G \cap I) \cup (G ∖ I)) = F \circ G$
3		coundi	$⊢ F \circ ((G \cap I) \cup (G ∖ I)) = (F \circ (G \cap I)) \cup (F \circ (G ∖ I))$
4	2 3	eqtr3i	$⊢ F \circ G = (F \circ (G \cap I)) \cup (F \circ (G ∖ I))$
5	4	difeq1i	$⊢ (F \circ G) ∖ I = ((F \circ (G \cap I)) \cup (F \circ (G ∖ I))) ∖ I$
6		difundir	$⊢ ((F \circ (G \cap I)) \cup (F \circ (G ∖ I))) ∖ I = ((F \circ (G \cap I)) ∖ I) \cup ((F \circ (G ∖ I)) ∖ I)$
7	5 6	eqtri	$⊢ (F \circ G) ∖ I = ((F \circ (G \cap I)) ∖ I) \cup ((F \circ (G ∖ I)) ∖ I)$
8	7	dmeqi	$⊢ dom ((F \circ G) ∖ I) = dom (((F \circ (G \cap I)) ∖ I) \cup ((F \circ (G ∖ I)) ∖ I))$
9		dmun	$⊢ dom (((F \circ (G \cap I)) ∖ I) \cup ((F \circ (G ∖ I)) ∖ I)) = dom ((F \circ (G \cap I)) ∖ I) \cup dom ((F \circ (G ∖ I)) ∖ I)$
10	8 9	eqtri	$⊢ dom ((F \circ G) ∖ I) = dom ((F \circ (G \cap I)) ∖ I) \cup dom ((F \circ (G ∖ I)) ∖ I)$
11		inss2	$⊢ G \cap I \subseteq I$
12		coss2	$⊢ G \cap I \subseteq I \to F \circ (G \cap I) \subseteq F \circ I$
13	11 12	ax-mp	$⊢ F \circ (G \cap I) \subseteq F \circ I$
14		cocnvcnv1	$⊢ {F^{-1}}^{-1} \circ I = F \circ I$
15		relcnv	$⊢ Rel {F^{-1}}^{-1}$
16		coi1	$⊢ Rel {F^{-1}}^{-1} \to {F^{-1}}^{-1} \circ I = {F^{-1}}^{-1}$
17	15 16	ax-mp	$⊢ {F^{-1}}^{-1} \circ I = {F^{-1}}^{-1}$
18	14 17	eqtr3i	$⊢ F \circ I = {F^{-1}}^{-1}$
19		cnvcnvss	$⊢ {F^{-1}}^{-1} \subseteq F$
20	18 19	eqsstri	$⊢ F \circ I \subseteq F$
21	13 20	sstri	$⊢ F \circ (G \cap I) \subseteq F$
22		ssdif	$⊢ F \circ (G \cap I) \subseteq F \to (F \circ (G \cap I)) ∖ I \subseteq F ∖ I$
23		dmss	$⊢ (F \circ (G \cap I)) ∖ I \subseteq F ∖ I \to dom ((F \circ (G \cap I)) ∖ I) \subseteq dom (F ∖ I)$
24	21 22 23	mp2b	$⊢ dom ((F \circ (G \cap I)) ∖ I) \subseteq dom (F ∖ I)$
25		difss	$⊢ (F \circ (G ∖ I)) ∖ I \subseteq F \circ (G ∖ I)$
26		dmss	$⊢ (F \circ (G ∖ I)) ∖ I \subseteq F \circ (G ∖ I) \to dom ((F \circ (G ∖ I)) ∖ I) \subseteq dom (F \circ (G ∖ I))$
27	25 26	ax-mp	$⊢ dom ((F \circ (G ∖ I)) ∖ I) \subseteq dom (F \circ (G ∖ I))$
28		dmcoss	$⊢ dom (F \circ (G ∖ I)) \subseteq dom (G ∖ I)$
29	27 28	sstri	$⊢ dom ((F \circ (G ∖ I)) ∖ I) \subseteq dom (G ∖ I)$
30		unss12	$⊢ (dom ((F \circ (G \cap I)) ∖ I) \subseteq dom (F ∖ I) \land dom ((F \circ (G ∖ I)) ∖ I) \subseteq dom (G ∖ I)) \to dom ((F \circ (G \cap I)) ∖ I) \cup dom ((F \circ (G ∖ I)) ∖ I) \subseteq dom (F ∖ I) \cup dom (G ∖ I)$
31	24 29 30	mp2an	$⊢ dom ((F \circ (G \cap I)) ∖ I) \cup dom ((F \circ (G ∖ I)) ∖ I) \subseteq dom (F ∖ I) \cup dom (G ∖ I)$
32	10 31	eqsstri	$⊢ dom ((F \circ G) ∖ I) \subseteq dom (F ∖ I) \cup dom (G ∖ I)$

Metamath Proof Explorer

Theorem mvdco

Proof