Step |
Hyp |
Ref |
Expression |
1 |
|
funssres |
|- ( ( Fun H /\ F C_ H ) -> ( H |` dom F ) = F ) |
2 |
1
|
ex |
|- ( Fun H -> ( F C_ H -> ( H |` dom F ) = F ) ) |
3 |
|
funssres |
|- ( ( Fun H /\ G C_ H ) -> ( H |` dom G ) = G ) |
4 |
3
|
ex |
|- ( Fun H -> ( G C_ H -> ( H |` dom G ) = G ) ) |
5 |
2 4
|
anim12d |
|- ( Fun H -> ( ( F C_ H /\ G C_ H ) -> ( ( H |` dom F ) = F /\ ( H |` dom G ) = G ) ) ) |
6 |
|
ssres2 |
|- ( dom F C_ dom G -> ( H |` dom F ) C_ ( H |` dom G ) ) |
7 |
|
ssres2 |
|- ( dom G C_ dom F -> ( H |` dom G ) C_ ( H |` dom F ) ) |
8 |
6 7
|
orim12i |
|- ( ( dom F C_ dom G \/ dom G C_ dom F ) -> ( ( H |` dom F ) C_ ( H |` dom G ) \/ ( H |` dom G ) C_ ( H |` dom F ) ) ) |
9 |
|
sseq12 |
|- ( ( ( H |` dom F ) = F /\ ( H |` dom G ) = G ) -> ( ( H |` dom F ) C_ ( H |` dom G ) <-> F C_ G ) ) |
10 |
|
sseq12 |
|- ( ( ( H |` dom G ) = G /\ ( H |` dom F ) = F ) -> ( ( H |` dom G ) C_ ( H |` dom F ) <-> G C_ F ) ) |
11 |
10
|
ancoms |
|- ( ( ( H |` dom F ) = F /\ ( H |` dom G ) = G ) -> ( ( H |` dom G ) C_ ( H |` dom F ) <-> G C_ F ) ) |
12 |
9 11
|
orbi12d |
|- ( ( ( H |` dom F ) = F /\ ( H |` dom G ) = G ) -> ( ( ( H |` dom F ) C_ ( H |` dom G ) \/ ( H |` dom G ) C_ ( H |` dom F ) ) <-> ( F C_ G \/ G C_ F ) ) ) |
13 |
8 12
|
syl5ib |
|- ( ( ( H |` dom F ) = F /\ ( H |` dom G ) = G ) -> ( ( dom F C_ dom G \/ dom G C_ dom F ) -> ( F C_ G \/ G C_ F ) ) ) |
14 |
5 13
|
syl6 |
|- ( Fun H -> ( ( F C_ H /\ G C_ H ) -> ( ( dom F C_ dom G \/ dom G C_ dom F ) -> ( F C_ G \/ G C_ F ) ) ) ) |
15 |
14
|
3imp |
|- ( ( Fun H /\ ( F C_ H /\ G C_ H ) /\ ( dom F C_ dom G \/ dom G C_ dom F ) ) -> ( F C_ G \/ G C_ F ) ) |
16 |
|
sspsstri |
|- ( ( F C_ G \/ G C_ F ) <-> ( F C. G \/ F = G \/ G C. F ) ) |
17 |
15 16
|
sylib |
|- ( ( Fun H /\ ( F C_ H /\ G C_ H ) /\ ( dom F C_ dom G \/ dom G C_ dom F ) ) -> ( F C. G \/ F = G \/ G C. F ) ) |