Metamath Proof Explorer

Theorem f1omvdco3

Description: If a point is moved by exactly one of two permutations, then it will be moved by their composite. (Contributed by Stefan O'Rear, 23-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 notbi 
 |-  ( ( X e. dom ( F \ _I ) <-> X e. dom ( G \ _I ) ) <-> ( -. X e. dom ( F \ _I ) <-> -. X e. dom ( G \ _I ) ) )
2 disjsn 
 |-  ( ( dom ( F \ _I ) i^i { X } ) = (/) <-> -. X e. dom ( F \ _I ) )
3 disj2 
 |-  ( ( dom ( F \ _I ) i^i { X } ) = (/) <-> dom ( F \ _I ) C_ ( _V \ { X } ) )
4 2 3 bitr3i 
 |-  ( -. X e. dom ( F \ _I ) <-> dom ( F \ _I ) C_ ( _V \ { X } ) )
5 disjsn 
 |-  ( ( dom ( G \ _I ) i^i { X } ) = (/) <-> -. X e. dom ( G \ _I ) )
6 disj2 
 |-  ( ( dom ( G \ _I ) i^i { X } ) = (/) <-> dom ( G \ _I ) C_ ( _V \ { X } ) )
7 5 6 bitr3i 
 |-  ( -. X e. dom ( G \ _I ) <-> dom ( G \ _I ) C_ ( _V \ { X } ) )
8 4 7 bibi12i 
 |-  ( ( -. X e. dom ( F \ _I ) <-> -. X e. dom ( G \ _I ) ) <-> ( dom ( F \ _I ) C_ ( _V \ { X } ) <-> dom ( G \ _I ) C_ ( _V \ { X } ) ) )
9 1 8 bitri 
 |-  ( ( X e. dom ( F \ _I ) <-> X e. dom ( G \ _I ) ) <-> ( dom ( F \ _I ) C_ ( _V \ { X } ) <-> dom ( G \ _I ) C_ ( _V \ { X } ) ) )
10 9 notbii 
 |-  ( -. ( X e. dom ( F \ _I ) <-> X e. dom ( G \ _I ) ) <-> -. ( dom ( F \ _I ) C_ ( _V \ { X } ) <-> dom ( G \ _I ) C_ ( _V \ { X } ) ) )
11 df-xor 
 |-  ( ( X e. dom ( F \ _I ) \/_ X e. dom ( G \ _I ) ) <-> -. ( X e. dom ( F \ _I ) <-> X e. dom ( G \ _I ) ) )
12 df-xor 
 |-  ( ( dom ( F \ _I ) C_ ( _V \ { X } ) \/_ dom ( G \ _I ) C_ ( _V \ { X } ) ) <-> -. ( dom ( F \ _I ) C_ ( _V \ { X } ) <-> dom ( G \ _I ) C_ ( _V \ { X } ) ) )
13 10 11 12 3bitr4i 
 |-  ( ( X e. dom ( F \ _I ) \/_ X e. dom ( G \ _I ) ) <-> ( dom ( F \ _I ) C_ ( _V \ { X } ) \/_ dom ( G \ _I ) C_ ( _V \ { X } ) ) )
14 f1omvdco2 
 |-  ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A /\ ( dom ( F \ _I ) C_ ( _V \ { X } ) \/_ dom ( G \ _I ) C_ ( _V \ { X } ) ) ) -> -. dom ( ( F o. G ) \ _I ) C_ ( _V \ { X } ) )
15 disj2 
 |-  ( ( dom ( ( F o. G ) \ _I ) i^i { X } ) = (/) <-> dom ( ( F o. G ) \ _I ) C_ ( _V \ { X } ) )
16 disjsn 
 |-  ( ( dom ( ( F o. G ) \ _I ) i^i { X } ) = (/) <-> -. X e. dom ( ( F o. G ) \ _I ) )
17 15 16 bitr3i 
 |-  ( dom ( ( F o. G ) \ _I ) C_ ( _V \ { X } ) <-> -. X e. dom ( ( F o. G ) \ _I ) )
18 17 con2bii 
 |-  ( X e. dom ( ( F o. G ) \ _I ) <-> -. dom ( ( F o. G ) \ _I ) C_ ( _V \ { X } ) )
19 14 18 sylibr 
 |-  ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A /\ ( dom ( F \ _I ) C_ ( _V \ { X } ) \/_ dom ( G \ _I ) C_ ( _V \ { X } ) ) ) -> X e. dom ( ( F o. G ) \ _I ) )
20 13 19 syl3an3b 
 |-  ( ( F : A -1-1-onto-> A /\ G : A -1-1-onto-> A /\ ( X e. dom ( F \ _I ) \/_ X e. dom ( G \ _I ) ) ) -> X e. dom ( ( F o. G ) \ _I ) )