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 𝑥 𝐵
Assertion fcomptf ( ( 𝐴 : 𝐷𝐸𝐵 : 𝐶𝐷 ) → ( 𝐴𝐵 ) = ( 𝑥𝐶 ↦ ( 𝐴 ‘ ( 𝐵𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 fcomptf.1 𝑥 𝐵
2 nfcv 𝑥 𝐴
3 nfcv 𝑥 𝐷
4 nfcv 𝑥 𝐸
5 2 3 4 nff 𝑥 𝐴 : 𝐷𝐸
6 nfcv 𝑥 𝐶
7 1 6 3 nff 𝑥 𝐵 : 𝐶𝐷
8 5 7 nfan 𝑥 ( 𝐴 : 𝐷𝐸𝐵 : 𝐶𝐷 )
9 ffvelrn ( ( 𝐵 : 𝐶𝐷𝑥𝐶 ) → ( 𝐵𝑥 ) ∈ 𝐷 )
10 9 adantll ( ( ( 𝐴 : 𝐷𝐸𝐵 : 𝐶𝐷 ) ∧ 𝑥𝐶 ) → ( 𝐵𝑥 ) ∈ 𝐷 )
11 10 ex ( ( 𝐴 : 𝐷𝐸𝐵 : 𝐶𝐷 ) → ( 𝑥𝐶 → ( 𝐵𝑥 ) ∈ 𝐷 ) )
12 8 11 ralrimi ( ( 𝐴 : 𝐷𝐸𝐵 : 𝐶𝐷 ) → ∀ 𝑥𝐶 ( 𝐵𝑥 ) ∈ 𝐷 )
13 ffn ( 𝐵 : 𝐶𝐷𝐵 Fn 𝐶 )
14 13 adantl ( ( 𝐴 : 𝐷𝐸𝐵 : 𝐶𝐷 ) → 𝐵 Fn 𝐶 )
15 1 dffn5f ( 𝐵 Fn 𝐶𝐵 = ( 𝑥𝐶 ↦ ( 𝐵𝑥 ) ) )
16 14 15 sylib ( ( 𝐴 : 𝐷𝐸𝐵 : 𝐶𝐷 ) → 𝐵 = ( 𝑥𝐶 ↦ ( 𝐵𝑥 ) ) )
17 ffn ( 𝐴 : 𝐷𝐸𝐴 Fn 𝐷 )
18 17 adantr ( ( 𝐴 : 𝐷𝐸𝐵 : 𝐶𝐷 ) → 𝐴 Fn 𝐷 )
19 dffn5 ( 𝐴 Fn 𝐷𝐴 = ( 𝑦𝐷 ↦ ( 𝐴𝑦 ) ) )
20 18 19 sylib ( ( 𝐴 : 𝐷𝐸𝐵 : 𝐶𝐷 ) → 𝐴 = ( 𝑦𝐷 ↦ ( 𝐴𝑦 ) ) )
21 fveq2 ( 𝑦 = ( 𝐵𝑥 ) → ( 𝐴𝑦 ) = ( 𝐴 ‘ ( 𝐵𝑥 ) ) )
22 12 16 20 21 fmptcof ( ( 𝐴 : 𝐷𝐸𝐵 : 𝐶𝐷 ) → ( 𝐴𝐵 ) = ( 𝑥𝐶 ↦ ( 𝐴 ‘ ( 𝐵𝑥 ) ) ) )