Step |
Hyp |
Ref |
Expression |
1 |
|
sbthlem.1 |
|- A e. _V |
2 |
|
sbthlem.2 |
|- D = { x | ( x C_ A /\ ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) ) } |
3 |
|
sbthlem.3 |
|- H = ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) ) |
4 |
|
funres11 |
|- ( Fun `' f -> Fun `' ( f |` U. D ) ) |
5 |
|
funcnvcnv |
|- ( Fun g -> Fun `' `' g ) |
6 |
|
funres11 |
|- ( Fun `' `' g -> Fun `' ( `' g |` ( A \ U. D ) ) ) |
7 |
5 6
|
syl |
|- ( Fun g -> Fun `' ( `' g |` ( A \ U. D ) ) ) |
8 |
7
|
ad3antrrr |
|- ( ( ( ( Fun g /\ dom g = B ) /\ ran g C_ A ) /\ Fun `' g ) -> Fun `' ( `' g |` ( A \ U. D ) ) ) |
9 |
4 8
|
anim12i |
|- ( ( Fun `' f /\ ( ( ( Fun g /\ dom g = B ) /\ ran g C_ A ) /\ Fun `' g ) ) -> ( Fun `' ( f |` U. D ) /\ Fun `' ( `' g |` ( A \ U. D ) ) ) ) |
10 |
|
df-ima |
|- ( f " U. D ) = ran ( f |` U. D ) |
11 |
|
df-rn |
|- ran ( f |` U. D ) = dom `' ( f |` U. D ) |
12 |
10 11
|
eqtr2i |
|- dom `' ( f |` U. D ) = ( f " U. D ) |
13 |
|
df-ima |
|- ( `' g " ( A \ U. D ) ) = ran ( `' g |` ( A \ U. D ) ) |
14 |
|
df-rn |
|- ran ( `' g |` ( A \ U. D ) ) = dom `' ( `' g |` ( A \ U. D ) ) |
15 |
13 14
|
eqtri |
|- ( `' g " ( A \ U. D ) ) = dom `' ( `' g |` ( A \ U. D ) ) |
16 |
1 2
|
sbthlem4 |
|- ( ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) -> ( `' g " ( A \ U. D ) ) = ( B \ ( f " U. D ) ) ) |
17 |
15 16
|
syl5eqr |
|- ( ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) -> dom `' ( `' g |` ( A \ U. D ) ) = ( B \ ( f " U. D ) ) ) |
18 |
|
ineq12 |
|- ( ( dom `' ( f |` U. D ) = ( f " U. D ) /\ dom `' ( `' g |` ( A \ U. D ) ) = ( B \ ( f " U. D ) ) ) -> ( dom `' ( f |` U. D ) i^i dom `' ( `' g |` ( A \ U. D ) ) ) = ( ( f " U. D ) i^i ( B \ ( f " U. D ) ) ) ) |
19 |
12 17 18
|
sylancr |
|- ( ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) -> ( dom `' ( f |` U. D ) i^i dom `' ( `' g |` ( A \ U. D ) ) ) = ( ( f " U. D ) i^i ( B \ ( f " U. D ) ) ) ) |
20 |
|
disjdif |
|- ( ( f " U. D ) i^i ( B \ ( f " U. D ) ) ) = (/) |
21 |
19 20
|
eqtrdi |
|- ( ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) -> ( dom `' ( f |` U. D ) i^i dom `' ( `' g |` ( A \ U. D ) ) ) = (/) ) |
22 |
21
|
adantlll |
|- ( ( ( ( Fun g /\ dom g = B ) /\ ran g C_ A ) /\ Fun `' g ) -> ( dom `' ( f |` U. D ) i^i dom `' ( `' g |` ( A \ U. D ) ) ) = (/) ) |
23 |
22
|
adantl |
|- ( ( Fun `' f /\ ( ( ( Fun g /\ dom g = B ) /\ ran g C_ A ) /\ Fun `' g ) ) -> ( dom `' ( f |` U. D ) i^i dom `' ( `' g |` ( A \ U. D ) ) ) = (/) ) |
24 |
|
funun |
|- ( ( ( Fun `' ( f |` U. D ) /\ Fun `' ( `' g |` ( A \ U. D ) ) ) /\ ( dom `' ( f |` U. D ) i^i dom `' ( `' g |` ( A \ U. D ) ) ) = (/) ) -> Fun ( `' ( f |` U. D ) u. `' ( `' g |` ( A \ U. D ) ) ) ) |
25 |
9 23 24
|
syl2anc |
|- ( ( Fun `' f /\ ( ( ( Fun g /\ dom g = B ) /\ ran g C_ A ) /\ Fun `' g ) ) -> Fun ( `' ( f |` U. D ) u. `' ( `' g |` ( A \ U. D ) ) ) ) |
26 |
3
|
cnveqi |
|- `' H = `' ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) ) |
27 |
|
cnvun |
|- `' ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) ) = ( `' ( f |` U. D ) u. `' ( `' g |` ( A \ U. D ) ) ) |
28 |
26 27
|
eqtri |
|- `' H = ( `' ( f |` U. D ) u. `' ( `' g |` ( A \ U. D ) ) ) |
29 |
28
|
funeqi |
|- ( Fun `' H <-> Fun ( `' ( f |` U. D ) u. `' ( `' g |` ( A \ U. D ) ) ) ) |
30 |
25 29
|
sylibr |
|- ( ( Fun `' f /\ ( ( ( Fun g /\ dom g = B ) /\ ran g C_ A ) /\ Fun `' g ) ) -> Fun `' H ) |