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 _ x B
Assertion fcomptf A : D E B : C D A B = x C A B x

Proof

Step Hyp Ref Expression
1 fcomptf.1 _ x B
2 nfcv _ x A
3 nfcv _ x D
4 nfcv _ x E
5 2 3 4 nff x A : D E
6 nfcv _ x C
7 1 6 3 nff x B : C D
8 5 7 nfan x A : D E B : C D
9 ffvelrn B : C D x C B x D
10 9 adantll A : D E B : C D x C B x D
11 10 ex A : D E B : C D x C B x D
12 8 11 ralrimi A : D E B : C D x C B x 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 C B x
16 14 15 sylib A : D E B : C D B = x 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 D A y
20 18 19 sylib A : D E B : C D A = y 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 B = x C A B x