Metamath Proof Explorer


Theorem fmpocos

Description: Composition of two functions. Variation of fmpoco with more context in the substitution hypothesis for T . (Contributed by SN, 14-Mar-2025)

Ref Expression
Hypotheses fmpocos.1 φ x A y B R C
fmpocos.2 φ F = x A , y B R
fmpocos.3 φ G = z C S
fmpocos.4 φ x A y B R / z S = T
Assertion fmpocos φ G F = x A , y B T

Proof

Step Hyp Ref Expression
1 fmpocos.1 φ x A y B R C
2 fmpocos.2 φ F = x A , y B R
3 fmpocos.3 φ G = z C S
4 fmpocos.4 φ x A y B R / z S = T
5 1 ralrimivva φ x A y B R C
6 eqid x A , y B R = x A , y B R
7 6 fmpo x A y B R C x A , y B R : A × B C
8 5 7 sylib φ x A , y B R : A × B C
9 nfcv _ u R
10 nfcv _ v R
11 nfcv _ x v
12 nfcsb1v _ x u / x R
13 11 12 nfcsbw _ x v / y u / x R
14 nfcsb1v _ y v / y u / x R
15 csbeq1a x = u R = u / x R
16 csbeq1a y = v u / x R = v / y u / x R
17 15 16 sylan9eq x = u y = v R = v / y u / x R
18 9 10 13 14 17 cbvmpo x A , y B R = u A , v B v / y u / x R
19 vex u V
20 vex v V
21 19 20 op2ndd w = u v 2 nd w = v
22 19 20 op1std w = u v 1 st w = u
23 22 csbeq1d w = u v 1 st w / x R = u / x R
24 21 23 csbeq12dv w = u v 2 nd w / y 1 st w / x R = v / y u / x R
25 24 mpompt w A × B 2 nd w / y 1 st w / x R = u A , v B v / y u / x R
26 18 25 eqtr4i x A , y B R = w A × B 2 nd w / y 1 st w / x R
27 26 fmpt w A × B 2 nd w / y 1 st w / x R C x A , y B R : A × B C
28 8 27 sylibr φ w A × B 2 nd w / y 1 st w / x R C
29 2 26 eqtrdi φ F = w A × B 2 nd w / y 1 st w / x R
30 28 29 3 fmptcos φ G F = w A × B 2 nd w / y 1 st w / x R / z S
31 24 csbeq1d w = u v 2 nd w / y 1 st w / x R / z S = v / y u / x R / z S
32 31 mpompt w A × B 2 nd w / y 1 st w / x R / z S = u A , v B v / y u / x R / z S
33 nfcv _ u R / z S
34 nfcv _ v R / z S
35 nfcv _ x S
36 13 35 nfcsbw _ x v / y u / x R / z S
37 nfcv _ y S
38 14 37 nfcsbw _ y v / y u / x R / z S
39 17 csbeq1d x = u y = v R / z S = v / y u / x R / z S
40 33 34 36 38 39 cbvmpo x A , y B R / z S = u A , v B v / y u / x R / z S
41 32 40 eqtr4i w A × B 2 nd w / y 1 st w / x R / z S = x A , y B R / z S
42 4 3impb φ x A y B R / z S = T
43 42 mpoeq3dva φ x A , y B R / z S = x A , y B T
44 41 43 eqtrid φ w A × B 2 nd w / y 1 st w / x R / z S = x A , y B T
45 30 44 eqtrd φ G F = x A , y B T