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 |
|
rnun |
|- ran ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) ) = ( ran ( f |` U. D ) u. ran ( `' g |` ( A \ U. D ) ) ) |
5 |
3
|
rneqi |
|- ran H = ran ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) ) |
6 |
|
df-ima |
|- ( f " U. D ) = ran ( f |` U. D ) |
7 |
6
|
uneq1i |
|- ( ( f " U. D ) u. ran ( `' g |` ( A \ U. D ) ) ) = ( ran ( f |` U. D ) u. ran ( `' g |` ( A \ U. D ) ) ) |
8 |
4 5 7
|
3eqtr4i |
|- ran H = ( ( f " U. D ) u. ran ( `' g |` ( A \ U. D ) ) ) |
9 |
1 2
|
sbthlem4 |
|- ( ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) -> ( `' g " ( A \ U. D ) ) = ( B \ ( f " U. D ) ) ) |
10 |
|
df-ima |
|- ( `' g " ( A \ U. D ) ) = ran ( `' g |` ( A \ U. D ) ) |
11 |
9 10
|
eqtr3di |
|- ( ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) -> ( B \ ( f " U. D ) ) = ran ( `' g |` ( A \ U. D ) ) ) |
12 |
11
|
uneq2d |
|- ( ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) -> ( ( f " U. D ) u. ( B \ ( f " U. D ) ) ) = ( ( f " U. D ) u. ran ( `' g |` ( A \ U. D ) ) ) ) |
13 |
8 12
|
eqtr4id |
|- ( ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) -> ran H = ( ( f " U. D ) u. ( B \ ( f " U. D ) ) ) ) |
14 |
|
imassrn |
|- ( f " U. D ) C_ ran f |
15 |
|
sstr2 |
|- ( ( f " U. D ) C_ ran f -> ( ran f C_ B -> ( f " U. D ) C_ B ) ) |
16 |
14 15
|
ax-mp |
|- ( ran f C_ B -> ( f " U. D ) C_ B ) |
17 |
|
undif |
|- ( ( f " U. D ) C_ B <-> ( ( f " U. D ) u. ( B \ ( f " U. D ) ) ) = B ) |
18 |
16 17
|
sylib |
|- ( ran f C_ B -> ( ( f " U. D ) u. ( B \ ( f " U. D ) ) ) = B ) |
19 |
13 18
|
sylan9eqr |
|- ( ( ran f C_ B /\ ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) ) -> ran H = B ) |