Metamath Proof Explorer

Theorem 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 o. G ) \ _I ) C_ ( dom ( F \ _I ) u. dom ( G \ _I ) )

Proof

Step Hyp Ref Expression
1 inundif 
 |-  ( ( G i^i _I ) u. ( G \ _I ) ) = G
2 1 coeq2i 
 |-  ( F o. ( ( G i^i _I ) u. ( G \ _I ) ) ) = ( F o. G )
3 coundi 
 |-  ( F o. ( ( G i^i _I ) u. ( G \ _I ) ) ) = ( ( F o. ( G i^i _I ) ) u. ( F o. ( G \ _I ) ) )
4 2 3 eqtr3i 
 |-  ( F o. G ) = ( ( F o. ( G i^i _I ) ) u. ( F o. ( G \ _I ) ) )
5 4 difeq1i 
 |-  ( ( F o. G ) \ _I ) = ( ( ( F o. ( G i^i _I ) ) u. ( F o. ( G \ _I ) ) ) \ _I )
6 difundir 
 |-  ( ( ( F o. ( G i^i _I ) ) u. ( F o. ( G \ _I ) ) ) \ _I ) = ( ( ( F o. ( G i^i _I ) ) \ _I ) u. ( ( F o. ( G \ _I ) ) \ _I ) )
7 5 6 eqtri 
 |-  ( ( F o. G ) \ _I ) = ( ( ( F o. ( G i^i _I ) ) \ _I ) u. ( ( F o. ( G \ _I ) ) \ _I ) )
8 7 dmeqi 
 |-  dom ( ( F o. G ) \ _I ) = dom ( ( ( F o. ( G i^i _I ) ) \ _I ) u. ( ( F o. ( G \ _I ) ) \ _I ) )
9 dmun 
 |-  dom ( ( ( F o. ( G i^i _I ) ) \ _I ) u. ( ( F o. ( G \ _I ) ) \ _I ) ) = ( dom ( ( F o. ( G i^i _I ) ) \ _I ) u. dom ( ( F o. ( G \ _I ) ) \ _I ) )
10 8 9 eqtri 
 |-  dom ( ( F o. G ) \ _I ) = ( dom ( ( F o. ( G i^i _I ) ) \ _I ) u. dom ( ( F o. ( G \ _I ) ) \ _I ) )
11 inss2 
 |-  ( G i^i _I ) C_ _I
12 coss2 
 |-  ( ( G i^i _I ) C_ _I -> ( F o. ( G i^i _I ) ) C_ ( F o. _I ) )
13 11 12 ax-mp 
 |-  ( F o. ( G i^i _I ) ) C_ ( F o. _I )
14 cocnvcnv1 
 |-  ( `' `' F o. _I ) = ( F o. _I )
15 relcnv 
 |-  Rel `' `' F
16 coi1 
 |-  ( Rel `' `' F -> ( `' `' F o. _I ) = `' `' F )
17 15 16 ax-mp 
 |-  ( `' `' F o. _I ) = `' `' F
18 14 17 eqtr3i 
 |-  ( F o. _I ) = `' `' F
19 cnvcnvss 
 |-  `' `' F C_ F
20 18 19 eqsstri 
 |-  ( F o. _I ) C_ F
21 13 20 sstri 
 |-  ( F o. ( G i^i _I ) ) C_ F
22 ssdif 
 |-  ( ( F o. ( G i^i _I ) ) C_ F -> ( ( F o. ( G i^i _I ) ) \ _I ) C_ ( F \ _I ) )
23 dmss 
 |-  ( ( ( F o. ( G i^i _I ) ) \ _I ) C_ ( F \ _I ) -> dom ( ( F o. ( G i^i _I ) ) \ _I ) C_ dom ( F \ _I ) )
24 21 22 23 mp2b 
 |-  dom ( ( F o. ( G i^i _I ) ) \ _I ) C_ dom ( F \ _I )
25 difss 
 |-  ( ( F o. ( G \ _I ) ) \ _I ) C_ ( F o. ( G \ _I ) )
26 dmss 
 |-  ( ( ( F o. ( G \ _I ) ) \ _I ) C_ ( F o. ( G \ _I ) ) -> dom ( ( F o. ( G \ _I ) ) \ _I ) C_ dom ( F o. ( G \ _I ) ) )
27 25 26 ax-mp 
 |-  dom ( ( F o. ( G \ _I ) ) \ _I ) C_ dom ( F o. ( G \ _I ) )
28 dmcoss 
 |-  dom ( F o. ( G \ _I ) ) C_ dom ( G \ _I )
29 27 28 sstri 
 |-  dom ( ( F o. ( G \ _I ) ) \ _I ) C_ dom ( G \ _I )
30 unss12 
 |-  ( ( dom ( ( F o. ( G i^i _I ) ) \ _I ) C_ dom ( F \ _I ) /\ dom ( ( F o. ( G \ _I ) ) \ _I ) C_ dom ( G \ _I ) ) -> ( dom ( ( F o. ( G i^i _I ) ) \ _I ) u. dom ( ( F o. ( G \ _I ) ) \ _I ) ) C_ ( dom ( F \ _I ) u. dom ( G \ _I ) ) )
31 24 29 30 mp2an 
 |-  ( dom ( ( F o. ( G i^i _I ) ) \ _I ) u. dom ( ( F o. ( G \ _I ) ) \ _I ) ) C_ ( dom ( F \ _I ) u. dom ( G \ _I ) )
32 10 31 eqsstri 
 |-  dom ( ( F o. G ) \ _I ) C_ ( dom ( F \ _I ) u. dom ( G \ _I ) )