Metamath Proof Explorer

Theorem f1omvdco2

Description: If exactly one of two permutations is limited to a set of points, then the composition will not be. (Contributed by Stefan O'Rear, 23-Aug-2015)

Ref Expression
Assertion f1omvdco2 
|- ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A /\ ( dom ( F \ _I ) C_ X \/_ dom ( G \ _I ) C_ X ) ) -> -. dom ( ( F o. G ) \ _I ) C_ X )

Proof

Step Hyp Ref Expression
1 excxor 
 |-  ( ( dom ( F \ _I ) C_ X \/_ dom ( G \ _I ) C_ X ) <-> ( ( dom ( F \ _I ) C_ X /\ -. dom ( G \ _I ) C_ X ) \/ ( -. dom ( F \ _I ) C_ X /\ dom ( G \ _I ) C_ X ) ) )
2 coass 
 |-  ( ( `' F o. F ) o. G ) = ( `' F o. ( F o. G ) )
3 f1ococnv1 
 |-  ( F : A -1-1-onto-> A -> ( `' F o. F ) = ( _I |` A ) )
4 3 coeq1d 
 |-  ( F : A -1-1-onto-> A -> ( ( `' F o. F ) o. G ) = ( ( _I |` A ) o. G ) )
5 f1of 
 |-  ( G : A -1-1-onto-> A -> G : A --> A )
6 fcoi2 
 |-  ( G : A --> A -> ( ( _I |` A ) o. G ) = G )
7 5 6 syl 
 |-  ( G : A -1-1-onto-> A -> ( ( _I |` A ) o. G ) = G )
8 4 7 sylan9eq 
 |-  ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) -> ( ( `' F o. F ) o. G ) = G )
9 2 8 syl5eqr 
 |-  ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) -> ( `' F o. ( F o. G ) ) = G )
10 9 difeq1d 
 |-  ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) -> ( ( `' F o. ( F o. G ) ) \ _I ) = ( G \ _I ) )
11 10 dmeqd 
 |-  ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) -> dom ( ( `' F o. ( F o. G ) ) \ _I ) = dom ( G \ _I ) )
12 11 adantr 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) C_ X /\ dom ( ( F o. G ) \ _I ) C_ X ) ) -> dom ( ( `' F o. ( F o. G ) ) \ _I ) = dom ( G \ _I ) )
13 mvdco 
 |-  dom ( ( `' F o. ( F o. G ) ) \ _I ) C_ ( dom ( `' F \ _I ) u. dom ( ( F o. G ) \ _I ) )
14 f1omvdcnv 
 |-  ( F : A -1-1-onto-> A -> dom ( `' F \ _I ) = dom ( F \ _I ) )
15 14 ad2antrr 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) C_ X /\ dom ( ( F o. G ) \ _I ) C_ X ) ) -> dom ( `' F \ _I ) = dom ( F \ _I ) )
16 simprl 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) C_ X /\ dom ( ( F o. G ) \ _I ) C_ X ) ) -> dom ( F \ _I ) C_ X )
17 15 16 eqsstrd 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) C_ X /\ dom ( ( F o. G ) \ _I ) C_ X ) ) -> dom ( `' F \ _I ) C_ X )
18 simprr 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) C_ X /\ dom ( ( F o. G ) \ _I ) C_ X ) ) -> dom ( ( F o. G ) \ _I ) C_ X )
19 17 18 unssd 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) C_ X /\ dom ( ( F o. G ) \ _I ) C_ X ) ) -> ( dom ( `' F \ _I ) u. dom ( ( F o. G ) \ _I ) ) C_ X )
20 13 19 sstrid 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) C_ X /\ dom ( ( F o. G ) \ _I ) C_ X ) ) -> dom ( ( `' F o. ( F o. G ) ) \ _I ) C_ X )
21 12 20 eqsstrrd 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( F \ _I ) C_ X /\ dom ( ( F o. G ) \ _I ) C_ X ) ) -> dom ( G \ _I ) C_ X )
22 21 expr 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ dom ( F \ _I ) C_ X ) -> ( dom ( ( F o. G ) \ _I ) C_ X -> dom ( G \ _I ) C_ X ) )
23 22 con3d 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ dom ( F \ _I ) C_ X ) -> ( -. dom ( G \ _I ) C_ X -> -. dom ( ( F o. G ) \ _I ) C_ X ) )
24 23 expimpd 
 |-  ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) -> ( ( dom ( F \ _I ) C_ X /\ -. dom ( G \ _I ) C_ X ) -> -. dom ( ( F o. G ) \ _I ) C_ X ) )
25 coass 
 |-  ( ( F o. G ) o. `' G ) = ( F o. ( G o. `' G ) )
26 f1ococnv2 
 |-  ( G : A -1-1-onto-> A -> ( G o. `' G ) = ( _I |` A ) )
27 26 coeq2d 
 |-  ( G : A -1-1-onto-> A -> ( F o. ( G o. `' G ) ) = ( F o. ( _I |` A ) ) )
28 f1of 
 |-  ( F : A -1-1-onto-> A -> F : A --> A )
29 fcoi1 
 |-  ( F : A --> A -> ( F o. ( _I |` A ) ) = F )
30 28 29 syl 
 |-  ( F : A -1-1-onto-> A -> ( F o. ( _I |` A ) ) = F )
31 27 30 sylan9eqr 
 |-  ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) -> ( F o. ( G o. `' G ) ) = F )
32 25 31 syl5eq 
 |-  ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) -> ( ( F o. G ) o. `' G ) = F )
33 32 difeq1d 
 |-  ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) -> ( ( ( F o. G ) o. `' G ) \ _I ) = ( F \ _I ) )
34 33 dmeqd 
 |-  ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) -> dom ( ( ( F o. G ) o. `' G ) \ _I ) = dom ( F \ _I ) )
35 34 adantr 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( G \ _I ) C_ X /\ dom ( ( F o. G ) \ _I ) C_ X ) ) -> dom ( ( ( F o. G ) o. `' G ) \ _I ) = dom ( F \ _I ) )
36 mvdco 
 |-  dom ( ( ( F o. G ) o. `' G ) \ _I ) C_ ( dom ( ( F o. G ) \ _I ) u. dom ( `' G \ _I ) )
37 simprr 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( G \ _I ) C_ X /\ dom ( ( F o. G ) \ _I ) C_ X ) ) -> dom ( ( F o. G ) \ _I ) C_ X )
38 f1omvdcnv 
 |-  ( G : A -1-1-onto-> A -> dom ( `' G \ _I ) = dom ( G \ _I ) )
39 38 ad2antlr 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( G \ _I ) C_ X /\ dom ( ( F o. G ) \ _I ) C_ X ) ) -> dom ( `' G \ _I ) = dom ( G \ _I ) )
40 simprl 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( G \ _I ) C_ X /\ dom ( ( F o. G ) \ _I ) C_ X ) ) -> dom ( G \ _I ) C_ X )
41 39 40 eqsstrd 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( G \ _I ) C_ X /\ dom ( ( F o. G ) \ _I ) C_ X ) ) -> dom ( `' G \ _I ) C_ X )
42 37 41 unssd 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( G \ _I ) C_ X /\ dom ( ( F o. G ) \ _I ) C_ X ) ) -> ( dom ( ( F o. G ) \ _I ) u. dom ( `' G \ _I ) ) C_ X )
43 36 42 sstrid 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( G \ _I ) C_ X /\ dom ( ( F o. G ) \ _I ) C_ X ) ) -> dom ( ( ( F o. G ) o. `' G ) \ _I ) C_ X )
44 35 43 eqsstrrd 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ ( dom ( G \ _I ) C_ X /\ dom ( ( F o. G ) \ _I ) C_ X ) ) -> dom ( F \ _I ) C_ X )
45 44 expr 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ dom ( G \ _I ) C_ X ) -> ( dom ( ( F o. G ) \ _I ) C_ X -> dom ( F \ _I ) C_ X ) )
46 45 con3d 
 |-  ( ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) /\ dom ( G \ _I ) C_ X ) -> ( -. dom ( F \ _I ) C_ X -> -. dom ( ( F o. G ) \ _I ) C_ X ) )
47 46 expimpd 
 |-  ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) -> ( ( dom ( G \ _I ) C_ X /\ -. dom ( F \ _I ) C_ X ) -> -. dom ( ( F o. G ) \ _I ) C_ X ) )
48 47 ancomsd 
 |-  ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) -> ( ( -. dom ( F \ _I ) C_ X /\ dom ( G \ _I ) C_ X ) -> -. dom ( ( F o. G ) \ _I ) C_ X ) )
49 24 48 jaod 
 |-  ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) -> ( ( ( dom ( F \ _I ) C_ X /\ -. dom ( G \ _I ) C_ X ) \/ ( -. dom ( F \ _I ) C_ X /\ dom ( G \ _I ) C_ X ) ) -> -. dom ( ( F o. G ) \ _I ) C_ X ) )
50 1 49 syl5bi 
 |-  ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A ) -> ( ( dom ( F \ _I ) C_ X \/_ dom ( G \ _I ) C_ X ) -> -. dom ( ( F o. G ) \ _I ) C_ X ) )
51 50 3impia 
 |-  ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A /\ ( dom ( F \ _I ) C_ X \/_ dom ( G \ _I ) C_ X ) ) -> -. dom ( ( F o. G ) \ _I ) C_ X )