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 ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ ( dom ( 𝐹 ∖ I ) ∪ dom ( 𝐺 ∖ I ) )

Proof

Step Hyp Ref Expression
1 inundif ⊢ ( ( 𝐺 ∩ I ) ∪ ( 𝐺 ∖ I ) ) = 𝐺
2 1 coeq2i ⊢ ( 𝐹 ∘ ( ( 𝐺 ∩ I ) ∪ ( 𝐺 ∖ I ) ) ) = ( 𝐹 ∘ 𝐺 )
3 coundi ⊢ ( 𝐹 ∘ ( ( 𝐺 ∩ I ) ∪ ( 𝐺 ∖ I ) ) ) = ( ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ∪ ( 𝐹 ∘ ( 𝐺 ∖ I ) ) )
4 2 3 eqtr3i ⊢ ( 𝐹 ∘ 𝐺 ) = ( ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ∪ ( 𝐹 ∘ ( 𝐺 ∖ I ) ) )
5 4 difeq1i ⊢ ( ( 𝐹 ∘ 𝐺 ) ∖ I ) = ( ( ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ∪ ( 𝐹 ∘ ( 𝐺 ∖ I ) ) ) ∖ I )
6 difundir ⊢ ( ( ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ∪ ( 𝐹 ∘ ( 𝐺 ∖ I ) ) ) ∖ I ) = ( ( ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ∖ I ) ∪ ( ( 𝐹 ∘ ( 𝐺 ∖ I ) ) ∖ I ) )
7 5 6 eqtri ⊢ ( ( 𝐹 ∘ 𝐺 ) ∖ I ) = ( ( ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ∖ I ) ∪ ( ( 𝐹 ∘ ( 𝐺 ∖ I ) ) ∖ I ) )
8 7 dmeqi ⊢ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) = dom ( ( ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ∖ I ) ∪ ( ( 𝐹 ∘ ( 𝐺 ∖ I ) ) ∖ I ) )
9 dmun ⊢ dom ( ( ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ∖ I ) ∪ ( ( 𝐹 ∘ ( 𝐺 ∖ I ) ) ∖ I ) ) = ( dom ( ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ∖ I ) ∪ dom ( ( 𝐹 ∘ ( 𝐺 ∖ I ) ) ∖ I ) )
10 8 9 eqtri ⊢ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) = ( dom ( ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ∖ I ) ∪ dom ( ( 𝐹 ∘ ( 𝐺 ∖ I ) ) ∖ I ) )
11 inss2 ⊢ ( 𝐺 ∩ I ) ⊆ I
12 coss2 ⊢ ( ( 𝐺 ∩ I ) ⊆ I → ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ⊆ ( 𝐹 ∘ I ) )
13 11 12 ax-mp ⊢ ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ⊆ ( 𝐹 ∘ I )
14 cocnvcnv1 ⊢ ( ◡ ◡ 𝐹 ∘ I ) = ( 𝐹 ∘ I )
15 relcnv ⊢ Rel ◡ ◡ 𝐹
16 coi1 ⊢ ( Rel ◡ ◡ 𝐹 → ( ◡ ◡ 𝐹 ∘ I ) = ◡ ◡ 𝐹 )
17 15 16 ax-mp ⊢ ( ◡ ◡ 𝐹 ∘ I ) = ◡ ◡ 𝐹
18 14 17 eqtr3i ⊢ ( 𝐹 ∘ I ) = ◡ ◡ 𝐹
19 cnvcnvss ⊢ ◡ ◡ 𝐹 ⊆ 𝐹
20 18 19 eqsstri ⊢ ( 𝐹 ∘ I ) ⊆ 𝐹
21 13 20 sstri ⊢ ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ⊆ 𝐹
22 ssdif ⊢ ( ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ⊆ 𝐹 → ( ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ∖ I ) ⊆ ( 𝐹 ∖ I ) )
23 dmss ⊢ ( ( ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ∖ I ) ⊆ ( 𝐹 ∖ I ) → dom ( ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ∖ I ) ⊆ dom ( 𝐹 ∖ I ) )
24 21 22 23 mp2b ⊢ dom ( ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ∖ I ) ⊆ dom ( 𝐹 ∖ I )
25 difss ⊢ ( ( 𝐹 ∘ ( 𝐺 ∖ I ) ) ∖ I ) ⊆ ( 𝐹 ∘ ( 𝐺 ∖ I ) )
26 dmss ⊢ ( ( ( 𝐹 ∘ ( 𝐺 ∖ I ) ) ∖ I ) ⊆ ( 𝐹 ∘ ( 𝐺 ∖ I ) ) → dom ( ( 𝐹 ∘ ( 𝐺 ∖ I ) ) ∖ I ) ⊆ dom ( 𝐹 ∘ ( 𝐺 ∖ I ) ) )
27 25 26 ax-mp ⊢ dom ( ( 𝐹 ∘ ( 𝐺 ∖ I ) ) ∖ I ) ⊆ dom ( 𝐹 ∘ ( 𝐺 ∖ I ) )
28 dmcoss ⊢ dom ( 𝐹 ∘ ( 𝐺 ∖ I ) ) ⊆ dom ( 𝐺 ∖ I )
29 27 28 sstri ⊢ dom ( ( 𝐹 ∘ ( 𝐺 ∖ I ) ) ∖ I ) ⊆ dom ( 𝐺 ∖ I )
30 unss12 ⊢ ( ( dom ( ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ∖ I ) ⊆ dom ( 𝐹 ∖ I ) ∧ dom ( ( 𝐹 ∘ ( 𝐺 ∖ I ) ) ∖ I ) ⊆ dom ( 𝐺 ∖ I ) ) → ( dom ( ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ∖ I ) ∪ dom ( ( 𝐹 ∘ ( 𝐺 ∖ I ) ) ∖ I ) ) ⊆ ( dom ( 𝐹 ∖ I ) ∪ dom ( 𝐺 ∖ I ) ) )
31 24 29 30 mp2an ⊢ ( dom ( ( 𝐹 ∘ ( 𝐺 ∩ I ) ) ∖ I ) ∪ dom ( ( 𝐹 ∘ ( 𝐺 ∖ I ) ) ∖ I ) ) ⊆ ( dom ( 𝐹 ∖ I ) ∪ dom ( 𝐺 ∖ I ) )
32 10 31 eqsstri ⊢ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ ( dom ( 𝐹 ∖ I ) ∪ dom ( 𝐺 ∖ I ) )