Metamath Proof Explorer

Theorem fcomptf

Description: Express composition of two functions as a maps-to applying both in sequence. This version has one less distinct variable restriction compared to fcompt . (Contributed by Thierry Arnoux, 30-Jun-2017)

Ref Expression
Hypothesis fcomptf.1 
|- F/_ x B
Assertion fcomptf 
|- ( ( A : D --> E /\ B : C --> D ) -> ( A o. B ) = ( x e. C |-> ( A ` ( B ` x ) ) ) )

Proof

Step Hyp Ref Expression
1 fcomptf.1 
 |-  F/_ x B
2 nfcv 
 |-  F/_ x A
3 nfcv 
 |-  F/_ x D
4 nfcv 
 |-  F/_ x E
5 2 3 4 nff 
 |-  F/ x A : D --> E
6 nfcv 
 |-  F/_ x C
7 1 6 3 nff 
 |-  F/ x B : C --> D
8 5 7 nfan 
 |-  F/ x ( A : D --> E /\ B : C --> D )
9 ffvelrn 
 |-  ( ( B : C --> D /\ x e. C ) -> ( B ` x ) e. D )
10 9 adantll 
 |-  ( ( ( A : D --> E /\ B : C --> D ) /\ x e. C ) -> ( B ` x ) e. D )
11 10 ex 
 |-  ( ( A : D --> E /\ B : C --> D ) -> ( x e. C -> ( B ` x ) e. D ) )
12 8 11 ralrimi 
 |-  ( ( A : D --> E /\ B : C --> D ) -> A. x e. C ( B ` x ) e. D )
13 ffn 
 |-  ( B : C --> D -> B Fn C )
14 13 adantl 
 |-  ( ( A : D --> E /\ B : C --> D ) -> B Fn C )
15 1 dffn5f 
 |-  ( B Fn C <-> B = ( x e. C |-> ( B ` x ) ) )
16 14 15 sylib 
 |-  ( ( A : D --> E /\ B : C --> D ) -> B = ( x e. C |-> ( B ` x ) ) )
17 ffn 
 |-  ( A : D --> E -> A Fn D )
18 17 adantr 
 |-  ( ( A : D --> E /\ B : C --> D ) -> A Fn D )
19 dffn5 
 |-  ( A Fn D <-> A = ( y e. D |-> ( A ` y ) ) )
20 18 19 sylib 
 |-  ( ( A : D --> E /\ B : C --> D ) -> A = ( y e. D |-> ( A ` y ) ) )
21 fveq2 
 |-  ( y = ( B ` x ) -> ( A ` y ) = ( A ` ( B ` x ) ) )
22 12 16 20 21 fmptcof 
 |-  ( ( A : D --> E /\ B : C --> D ) -> ( A o. B ) = ( x e. C |-> ( A ` ( B ` x ) ) ) )