Metamath Proof Explorer


Theorem sbthlem8

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 sbthlem8
|- ( ( Fun `' f /\ ( ( ( Fun g /\ dom g = B ) /\ ran g C_ A ) /\ 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 funres11
 |-  ( Fun `' f -> Fun `' ( f |` U. D ) )
5 funcnvcnv
 |-  ( Fun g -> Fun `' `' g )
6 funres11
 |-  ( Fun `' `' g -> Fun `' ( `' g |` ( A \ U. D ) ) )
7 5 6 syl
 |-  ( Fun g -> Fun `' ( `' g |` ( A \ U. D ) ) )
8 7 ad3antrrr
 |-  ( ( ( ( Fun g /\ dom g = B ) /\ ran g C_ A ) /\ Fun `' g ) -> Fun `' ( `' g |` ( A \ U. D ) ) )
9 4 8 anim12i
 |-  ( ( Fun `' f /\ ( ( ( Fun g /\ dom g = B ) /\ ran g C_ A ) /\ Fun `' g ) ) -> ( Fun `' ( f |` U. D ) /\ Fun `' ( `' g |` ( A \ U. D ) ) ) )
10 df-ima
 |-  ( f " U. D ) = ran ( f |` U. D )
11 df-rn
 |-  ran ( f |` U. D ) = dom `' ( f |` U. D )
12 10 11 eqtr2i
 |-  dom `' ( f |` U. D ) = ( f " U. D )
13 df-ima
 |-  ( `' g " ( A \ U. D ) ) = ran ( `' g |` ( A \ U. D ) )
14 df-rn
 |-  ran ( `' g |` ( A \ U. D ) ) = dom `' ( `' g |` ( A \ U. D ) )
15 13 14 eqtri
 |-  ( `' g " ( A \ U. D ) ) = dom `' ( `' g |` ( A \ U. D ) )
16 1 2 sbthlem4
 |-  ( ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) -> ( `' g " ( A \ U. D ) ) = ( B \ ( f " U. D ) ) )
17 15 16 eqtr3id
 |-  ( ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) -> dom `' ( `' g |` ( A \ U. D ) ) = ( B \ ( f " U. D ) ) )
18 ineq12
 |-  ( ( dom `' ( f |` U. D ) = ( f " U. D ) /\ dom `' ( `' g |` ( A \ U. D ) ) = ( B \ ( f " U. D ) ) ) -> ( dom `' ( f |` U. D ) i^i dom `' ( `' g |` ( A \ U. D ) ) ) = ( ( f " U. D ) i^i ( B \ ( f " U. D ) ) ) )
19 12 17 18 sylancr
 |-  ( ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) -> ( dom `' ( f |` U. D ) i^i dom `' ( `' g |` ( A \ U. D ) ) ) = ( ( f " U. D ) i^i ( B \ ( f " U. D ) ) ) )
20 disjdif
 |-  ( ( f " U. D ) i^i ( B \ ( f " U. D ) ) ) = (/)
21 19 20 eqtrdi
 |-  ( ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) -> ( dom `' ( f |` U. D ) i^i dom `' ( `' g |` ( A \ U. D ) ) ) = (/) )
22 21 adantlll
 |-  ( ( ( ( Fun g /\ dom g = B ) /\ ran g C_ A ) /\ Fun `' g ) -> ( dom `' ( f |` U. D ) i^i dom `' ( `' g |` ( A \ U. D ) ) ) = (/) )
23 22 adantl
 |-  ( ( Fun `' f /\ ( ( ( Fun g /\ dom g = B ) /\ ran g C_ A ) /\ Fun `' g ) ) -> ( dom `' ( f |` U. D ) i^i dom `' ( `' g |` ( A \ U. D ) ) ) = (/) )
24 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 ) ) ) )
25 9 23 24 syl2anc
 |-  ( ( Fun `' f /\ ( ( ( Fun g /\ dom g = B ) /\ ran g C_ A ) /\ Fun `' g ) ) -> Fun ( `' ( f |` U. D ) u. `' ( `' g |` ( A \ U. D ) ) ) )
26 3 cnveqi
 |-  `' H = `' ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) )
27 cnvun
 |-  `' ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) ) = ( `' ( f |` U. D ) u. `' ( `' g |` ( A \ U. D ) ) )
28 26 27 eqtri
 |-  `' H = ( `' ( f |` U. D ) u. `' ( `' g |` ( A \ U. D ) ) )
29 28 funeqi
 |-  ( Fun `' H <-> Fun ( `' ( f |` U. D ) u. `' ( `' g |` ( A \ U. D ) ) ) )
30 25 29 sylibr
 |-  ( ( Fun `' f /\ ( ( ( Fun g /\ dom g = B ) /\ ran g C_ A ) /\ Fun `' g ) ) -> Fun `' H )