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 )