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 ) )