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