Metamath Proof Explorer

Theorem sbthlem5

Description: Lemma for sbth . (Contributed by NM, 22-Mar-1998)

Ref Expression
Hypotheses sbthlem.1 
|- A e. _V
sbthlem.2 
|- D = { x | ( x C_ A /\ ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) ) }
sbthlem.3 
|- H = ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) )
Assertion sbthlem5 
|- ( ( dom f = A /\ ran g C_ A ) -> dom H = A )

Proof

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 3 dmeqi 
 |-  dom H = dom ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) )
5 dmun 
 |-  dom ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) ) = ( dom ( f |` U. D ) u. dom ( `' g |` ( A \ U. D ) ) )
6 dmres 
 |-  dom ( f |` U. D ) = ( U. D i^i dom f )
7 dmres 
 |-  dom ( `' g |` ( A \ U. D ) ) = ( ( A \ U. D ) i^i dom `' g )
8 df-rn 
 |-  ran g = dom `' g
9 8 eqcomi 
 |-  dom `' g = ran g
10 9 ineq2i 
 |-  ( ( A \ U. D ) i^i dom `' g ) = ( ( A \ U. D ) i^i ran g )
11 7 10 eqtri 
 |-  dom ( `' g |` ( A \ U. D ) ) = ( ( A \ U. D ) i^i ran g )
12 6 11 uneq12i 
 |-  ( dom ( f |` U. D ) u. dom ( `' g |` ( A \ U. D ) ) ) = ( ( U. D i^i dom f ) u. ( ( A \ U. D ) i^i ran g ) )
13 5 12 eqtri 
 |-  dom ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) ) = ( ( U. D i^i dom f ) u. ( ( A \ U. D ) i^i ran g ) )
14 4 13 eqtri 
 |-  dom H = ( ( U. D i^i dom f ) u. ( ( A \ U. D ) i^i ran g ) )
15 1 2 sbthlem1 
 |-  U. D C_ ( A \ ( g " ( B \ ( f " U. D ) ) ) )
16 difss 
 |-  ( A \ ( g " ( B \ ( f " U. D ) ) ) ) C_ A
17 15 16 sstri 
 |-  U. D C_ A
18 sseq2 
 |-  ( dom f = A -> ( U. D C_ dom f <-> U. D C_ A ) )
19 17 18 mpbiri 
 |-  ( dom f = A -> U. D C_ dom f )
20 dfss 
 |-  ( U. D C_ dom f <-> U. D = ( U. D i^i dom f ) )
21 19 20 sylib 
 |-  ( dom f = A -> U. D = ( U. D i^i dom f ) )
22 21 uneq1d 
 |-  ( dom f = A -> ( U. D u. ( A \ U. D ) ) = ( ( U. D i^i dom f ) u. ( A \ U. D ) ) )
23 1 2 sbthlem3 
 |-  ( ran g C_ A -> ( g " ( B \ ( f " U. D ) ) ) = ( A \ U. D ) )
24 imassrn 
 |-  ( g " ( B \ ( f " U. D ) ) ) C_ ran g
25 23 24 eqsstrrdi 
 |-  ( ran g C_ A -> ( A \ U. D ) C_ ran g )
26 dfss 
 |-  ( ( A \ U. D ) C_ ran g <-> ( A \ U. D ) = ( ( A \ U. D ) i^i ran g ) )
27 25 26 sylib 
 |-  ( ran g C_ A -> ( A \ U. D ) = ( ( A \ U. D ) i^i ran g ) )
28 27 uneq2d 
 |-  ( ran g C_ A -> ( ( U. D i^i dom f ) u. ( A \ U. D ) ) = ( ( U. D i^i dom f ) u. ( ( A \ U. D ) i^i ran g ) ) )
29 22 28 sylan9eq 
 |-  ( ( dom f = A /\ ran g C_ A ) -> ( U. D u. ( A \ U. D ) ) = ( ( U. D i^i dom f ) u. ( ( A \ U. D ) i^i ran g ) ) )
30 14 29 eqtr4id 
 |-  ( ( dom f = A /\ ran g C_ A ) -> dom H = ( U. D u. ( A \ U. D ) ) )
31 undif 
 |-  ( U. D C_ A <-> ( U. D u. ( A \ U. D ) ) = A )
32 17 31 mpbi 
 |-  ( U. D u. ( A \ U. D ) ) = A
33 30 32 eqtrdi 
 |-  ( ( dom f = A /\ ran g C_ A ) -> dom H = A )