| 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 |
1 2
|
sbthlem2 |
|- ( ran g C_ A -> ( A \ ( g " ( B \ ( f " U. D ) ) ) ) C_ U. D ) |
| 4 |
1 2
|
sbthlem1 |
|- U. D C_ ( A \ ( g " ( B \ ( f " U. D ) ) ) ) |
| 5 |
3 4
|
jctil |
|- ( ran g C_ A -> ( U. D C_ ( A \ ( g " ( B \ ( f " U. D ) ) ) ) /\ ( A \ ( g " ( B \ ( f " U. D ) ) ) ) C_ U. D ) ) |
| 6 |
|
eqss |
|- ( U. D = ( A \ ( g " ( B \ ( f " U. D ) ) ) ) <-> ( U. D C_ ( A \ ( g " ( B \ ( f " U. D ) ) ) ) /\ ( A \ ( g " ( B \ ( f " U. D ) ) ) ) C_ U. D ) ) |
| 7 |
5 6
|
sylibr |
|- ( ran g C_ A -> U. D = ( A \ ( g " ( B \ ( f " U. D ) ) ) ) ) |
| 8 |
7
|
difeq2d |
|- ( ran g C_ A -> ( A \ U. D ) = ( A \ ( A \ ( g " ( B \ ( f " U. D ) ) ) ) ) ) |
| 9 |
|
imassrn |
|- ( g " ( B \ ( f " U. D ) ) ) C_ ran g |
| 10 |
|
sstr2 |
|- ( ( g " ( B \ ( f " U. D ) ) ) C_ ran g -> ( ran g C_ A -> ( g " ( B \ ( f " U. D ) ) ) C_ A ) ) |
| 11 |
9 10
|
ax-mp |
|- ( ran g C_ A -> ( g " ( B \ ( f " U. D ) ) ) C_ A ) |
| 12 |
|
dfss4 |
|- ( ( g " ( B \ ( f " U. D ) ) ) C_ A <-> ( A \ ( A \ ( g " ( B \ ( f " U. D ) ) ) ) ) = ( g " ( B \ ( f " U. D ) ) ) ) |
| 13 |
11 12
|
sylib |
|- ( ran g C_ A -> ( A \ ( A \ ( g " ( B \ ( f " U. D ) ) ) ) ) = ( g " ( B \ ( f " U. D ) ) ) ) |
| 14 |
8 13
|
eqtr2d |
|- ( ran g C_ A -> ( g " ( B \ ( f " U. D ) ) ) = ( A \ U. D ) ) |