Metamath Proof Explorer

Theorem sbthlem7

Description: Lemma for sbth . (Contributed by NM, 27-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 sbthlem7 
|- ( ( Fun f /\ Fun `' g ) -> Fun H )

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 funres 
 |-  ( Fun f -> Fun ( f |` U. D ) )
5 funres 
 |-  ( Fun `' g -> Fun ( `' g |` ( A \ U. D ) ) )
6 dmres 
 |-  dom ( f |` U. D ) = ( U. D i^i dom f )
7 inss1 
 |-  ( U. D i^i dom f ) C_ U. D
8 6 7 eqsstri 
 |-  dom ( f |` U. D ) C_ U. D
9 ssrin 
 |-  ( dom ( f |` U. D ) C_ U. D -> ( dom ( f |` U. D ) i^i dom ( `' g |` ( A \ U. D ) ) ) C_ ( U. D i^i dom ( `' g |` ( A \ U. D ) ) ) )
10 8 9 ax-mp 
 |-  ( dom ( f |` U. D ) i^i dom ( `' g |` ( A \ U. D ) ) ) C_ ( U. D i^i dom ( `' g |` ( A \ U. D ) ) )
11 dmres 
 |-  dom ( `' g |` ( A \ U. D ) ) = ( ( A \ U. D ) i^i dom `' g )
12 inss1 
 |-  ( ( A \ U. D ) i^i dom `' g ) C_ ( A \ U. D )
13 11 12 eqsstri 
 |-  dom ( `' g |` ( A \ U. D ) ) C_ ( A \ U. D )
14 sslin 
 |-  ( dom ( `' g |` ( A \ U. D ) ) C_ ( A \ U. D ) -> ( U. D i^i dom ( `' g |` ( A \ U. D ) ) ) C_ ( U. D i^i ( A \ U. D ) ) )
15 13 14 ax-mp 
 |-  ( U. D i^i dom ( `' g |` ( A \ U. D ) ) ) C_ ( U. D i^i ( A \ U. D ) )
16 10 15 sstri 
 |-  ( dom ( f |` U. D ) i^i dom ( `' g |` ( A \ U. D ) ) ) C_ ( U. D i^i ( A \ U. D ) )
17 disjdif 
 |-  ( U. D i^i ( A \ U. D ) ) = (/)
18 16 17 sseqtri 
 |-  ( dom ( f |` U. D ) i^i dom ( `' g |` ( A \ U. D ) ) ) C_ (/)
19 ss0 
 |-  ( ( dom ( f |` U. D ) i^i dom ( `' g |` ( A \ U. D ) ) ) C_ (/) -> ( dom ( f |` U. D ) i^i dom ( `' g |` ( A \ U. D ) ) ) = (/) )
20 18 19 ax-mp 
 |-  ( dom ( f |` U. D ) i^i dom ( `' g |` ( A \ U. D ) ) ) = (/)
21 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 ) ) ) )
22 20 21 mpan2 
 |-  ( ( Fun ( f |` U. D ) /\ Fun ( `' g |` ( A \ U. D ) ) ) -> Fun ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) ) )
23 4 5 22 syl2an 
 |-  ( ( Fun f /\ Fun `' g ) -> Fun ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) ) )
24 3 funeqi 
 |-  ( Fun H <-> Fun ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) ) )
25 23 24 sylibr 
 |-  ( ( Fun f /\ Fun `' g ) -> Fun H )