# Metamath Proof Explorer

## Theorem fmptco

Description: Composition of two functions expressed as ordered-pair class abstractions. If F has the equation ( x + 2 ) and G the equation ( 3 * z ) then ( G o. F ) has the equation ( 3 * ( x + 2 ) ) . (Contributed by FL, 21-Jun-2012) (Revised by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses fmptco.1 $⊢ φ ∧ x ∈ A → R ∈ B$
fmptco.2 $⊢ φ → F = x ∈ A ⟼ R$
fmptco.3 $⊢ φ → G = y ∈ B ⟼ S$
fmptco.4 $⊢ y = R → S = T$
Assertion fmptco $⊢ φ → G ∘ F = x ∈ A ⟼ T$

### Proof

Step Hyp Ref Expression
1 fmptco.1 $⊢ φ ∧ x ∈ A → R ∈ B$
2 fmptco.2 $⊢ φ → F = x ∈ A ⟼ R$
3 fmptco.3 $⊢ φ → G = y ∈ B ⟼ S$
4 fmptco.4 $⊢ y = R → S = T$
5 relco $⊢ Rel ⁡ G ∘ F$
6 mptrel $⊢ Rel ⁡ x ∈ A ⟼ T$
7 2 1 fmpt3d $⊢ φ → F : A ⟶ B$
8 7 ffund $⊢ φ → Fun ⁡ F$
9 funbrfv $⊢ Fun ⁡ F → z F u → F ⁡ z = u$
10 9 imp $⊢ Fun ⁡ F ∧ z F u → F ⁡ z = u$
11 8 10 sylan $⊢ φ ∧ z F u → F ⁡ z = u$
12 11 eqcomd $⊢ φ ∧ z F u → u = F ⁡ z$
13 12 a1d $⊢ φ ∧ z F u → u G w → u = F ⁡ z$
14 13 expimpd $⊢ φ → z F u ∧ u G w → u = F ⁡ z$
15 14 pm4.71rd $⊢ φ → z F u ∧ u G w ↔ u = F ⁡ z ∧ z F u ∧ u G w$
16 15 exbidv $⊢ φ → ∃ u z F u ∧ u G w ↔ ∃ u u = F ⁡ z ∧ z F u ∧ u G w$
17 fvex $⊢ F ⁡ z ∈ V$
18 breq2 $⊢ u = F ⁡ z → z F u ↔ z F F ⁡ z$
19 breq1 $⊢ u = F ⁡ z → u G w ↔ F ⁡ z G w$
20 18 19 anbi12d $⊢ u = F ⁡ z → z F u ∧ u G w ↔ z F F ⁡ z ∧ F ⁡ z G w$
21 17 20 ceqsexv $⊢ ∃ u u = F ⁡ z ∧ z F u ∧ u G w ↔ z F F ⁡ z ∧ F ⁡ z G w$
22 funfvbrb $⊢ Fun ⁡ F → z ∈ dom ⁡ F ↔ z F F ⁡ z$
23 8 22 syl $⊢ φ → z ∈ dom ⁡ F ↔ z F F ⁡ z$
24 7 fdmd $⊢ φ → dom ⁡ F = A$
25 24 eleq2d $⊢ φ → z ∈ dom ⁡ F ↔ z ∈ A$
26 23 25 bitr3d $⊢ φ → z F F ⁡ z ↔ z ∈ A$
27 2 fveq1d $⊢ φ → F ⁡ z = x ∈ A ⟼ R ⁡ z$
28 eqidd $⊢ φ → w = w$
29 27 3 28 breq123d $⊢ φ → F ⁡ z G w ↔ x ∈ A ⟼ R ⁡ z y ∈ B ⟼ S w$
30 26 29 anbi12d $⊢ φ → z F F ⁡ z ∧ F ⁡ z G w ↔ z ∈ A ∧ x ∈ A ⟼ R ⁡ z y ∈ B ⟼ S w$
31 nfcv $⊢ Ⅎ _ x z$
32 nfv $⊢ Ⅎ x φ$
33 nffvmpt1 $⊢ Ⅎ _ x x ∈ A ⟼ R ⁡ z$
34 nfcv $⊢ Ⅎ _ x y ∈ B ⟼ S$
35 nfcv $⊢ Ⅎ _ x w$
36 33 34 35 nfbr $⊢ Ⅎ x x ∈ A ⟼ R ⁡ z y ∈ B ⟼ S w$
37 nfcsb1v
38 37 nfeq2
39 36 38 nfbi
40 32 39 nfim
41 fveq2 $⊢ x = z → x ∈ A ⟼ R ⁡ x = x ∈ A ⟼ R ⁡ z$
42 41 breq1d $⊢ x = z → x ∈ A ⟼ R ⁡ x y ∈ B ⟼ S w ↔ x ∈ A ⟼ R ⁡ z y ∈ B ⟼ S w$
43 csbeq1a
44 43 eqeq2d
45 42 44 bibi12d
46 45 imbi2d
47 vex $⊢ w ∈ V$
48 simpl $⊢ y = R ∧ u = w → y = R$
49 48 eleq1d $⊢ y = R ∧ u = w → y ∈ B ↔ R ∈ B$
50 id $⊢ u = w → u = w$
51 50 4 eqeqan12rd $⊢ y = R ∧ u = w → u = S ↔ w = T$
52 49 51 anbi12d $⊢ y = R ∧ u = w → y ∈ B ∧ u = S ↔ R ∈ B ∧ w = T$
53 df-mpt $⊢ y ∈ B ⟼ S = y u | y ∈ B ∧ u = S$
54 52 53 brabga $⊢ R ∈ B ∧ w ∈ V → R y ∈ B ⟼ S w ↔ R ∈ B ∧ w = T$
55 1 47 54 sylancl $⊢ φ ∧ x ∈ A → R y ∈ B ⟼ S w ↔ R ∈ B ∧ w = T$
56 id $⊢ x ∈ A → x ∈ A$
57 eqid $⊢ x ∈ A ⟼ R = x ∈ A ⟼ R$
58 57 fvmpt2 $⊢ x ∈ A ∧ R ∈ B → x ∈ A ⟼ R ⁡ x = R$
59 56 1 58 syl2an2 $⊢ φ ∧ x ∈ A → x ∈ A ⟼ R ⁡ x = R$
60 59 breq1d $⊢ φ ∧ x ∈ A → x ∈ A ⟼ R ⁡ x y ∈ B ⟼ S w ↔ R y ∈ B ⟼ S w$
61 1 biantrurd $⊢ φ ∧ x ∈ A → w = T ↔ R ∈ B ∧ w = T$
62 55 60 61 3bitr4d $⊢ φ ∧ x ∈ A → x ∈ A ⟼ R ⁡ x y ∈ B ⟼ S w ↔ w = T$
63 62 expcom $⊢ x ∈ A → φ → x ∈ A ⟼ R ⁡ x y ∈ B ⟼ S w ↔ w = T$
64 31 40 46 63 vtoclgaf
65 64 impcom
66 65 pm5.32da
67 30 66 bitrd
68 21 67 syl5bb
69 16 68 bitrd
70 vex $⊢ z ∈ V$
71 70 47 opelco $⊢ z w ∈ G ∘ F ↔ ∃ u z F u ∧ u G w$
72 df-mpt $⊢ x ∈ A ⟼ T = x v | x ∈ A ∧ v = T$
73 72 eleq2i $⊢ z w ∈ x ∈ A ⟼ T ↔ z w ∈ x v | x ∈ A ∧ v = T$
74 nfv $⊢ Ⅎ x z ∈ A$
75 37 nfeq2
76 74 75 nfan
77 nfv
78 eleq1w $⊢ x = z → x ∈ A ↔ z ∈ A$
79 43 eqeq2d
80 78 79 anbi12d
81 eqeq1
82 81 anbi2d
83 76 77 70 47 80 82 opelopabf
84 73 83 bitri
85 69 71 84 3bitr4g $⊢ φ → z w ∈ G ∘ F ↔ z w ∈ x ∈ A ⟼ T$
86 5 6 85 eqrelrdv $⊢ φ → G ∘ F = x ∈ A ⟼ T$