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:A1-1 ontoAG:A1-1 ontoAXdomFIXdomGIXdomFGI

Proof

Step Hyp Ref Expression
1 notbi XdomFIXdomGI¬XdomFI¬XdomGI
2 disjsn domFIX=¬XdomFI
3 disj2 domFIX=domFIVX
4 2 3 bitr3i ¬XdomFIdomFIVX
5 disjsn domGIX=¬XdomGI
6 disj2 domGIX=domGIVX
7 5 6 bitr3i ¬XdomGIdomGIVX
8 4 7 bibi12i ¬XdomFI¬XdomGIdomFIVXdomGIVX
9 1 8 bitri XdomFIXdomGIdomFIVXdomGIVX
10 9 notbii ¬XdomFIXdomGI¬domFIVXdomGIVX
11 df-xor XdomFIXdomGI¬XdomFIXdomGI
12 df-xor domFIVXdomGIVX¬domFIVXdomGIVX
13 10 11 12 3bitr4i XdomFIXdomGIdomFIVXdomGIVX
14 f1omvdco2 F:A1-1 ontoAG:A1-1 ontoAdomFIVXdomGIVX¬domFGIVX
15 disj2 domFGIX=domFGIVX
16 disjsn domFGIX=¬XdomFGI
17 15 16 bitr3i domFGIVX¬XdomFGI
18 17 con2bii XdomFGI¬domFGIVX
19 14 18 sylibr F:A1-1 ontoAG:A1-1 ontoAdomFIVXdomGIVXXdomFGI
20 13 19 syl3an3b F:A1-1 ontoAG:A1-1 ontoAXdomFIXdomGIXdomFGI