# 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 )`