This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑅 ∈ 𝐵 )
fmptco.2 ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) )
fmptco.3 ⊢ ( 𝜑 → 𝐺 = ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) )
fmptco.4 ⊢ ( 𝑦 = 𝑅 → 𝑆 = 𝑇 )
Assertion fmptco ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 fmptco.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑅 ∈ 𝐵 )
2 fmptco.2 ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) )
3 fmptco.3 ⊢ ( 𝜑 → 𝐺 = ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) )
4 fmptco.4 ⊢ ( 𝑦 = 𝑅 → 𝑆 = 𝑇 )
5 relco ⊢ Rel ( 𝐺 ∘ 𝐹 )
6 mptrel ⊢ Rel ( 𝑥 ∈ 𝐴 ↦ 𝑇 )
7 2 1 fmpt3d ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
8 7 ffund ⊢ ( 𝜑 → Fun 𝐹 )
9 funbrfv ⊢ ( Fun 𝐹 → ( 𝑧 𝐹 𝑢 → ( 𝐹 ‘ 𝑧 ) = 𝑢 ) )
10 9 imp ⊢ ( ( Fun 𝐹 ∧ 𝑧 𝐹 𝑢 ) → ( 𝐹 ‘ 𝑧 ) = 𝑢 )
11 8 10 sylan ⊢ ( ( 𝜑 ∧ 𝑧 𝐹 𝑢 ) → ( 𝐹 ‘ 𝑧 ) = 𝑢 )
12 11 eqcomd ⊢ ( ( 𝜑 ∧ 𝑧 𝐹 𝑢 ) → 𝑢 = ( 𝐹 ‘ 𝑧 ) )
13 12 a1d ⊢ ( ( 𝜑 ∧ 𝑧 𝐹 𝑢 ) → ( 𝑢 𝐺 𝑤 → 𝑢 = ( 𝐹 ‘ 𝑧 ) ) )
14 13 expimpd ⊢ ( 𝜑 → ( ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) → 𝑢 = ( 𝐹 ‘ 𝑧 ) ) )
15 14 pm4.71rd ⊢ ( 𝜑 → ( ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) ↔ ( 𝑢 = ( 𝐹 ‘ 𝑧 ) ∧ ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) ) ) )
16 15 exbidv ⊢ ( 𝜑 → ( ∃ 𝑢 ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) ↔ ∃ 𝑢 ( 𝑢 = ( 𝐹 ‘ 𝑧 ) ∧ ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) ) ) )
17 fvex ⊢ ( 𝐹 ‘ 𝑧 ) ∈ V
18 breq2 ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑧 ) → ( 𝑧 𝐹 𝑢 ↔ 𝑧 𝐹 ( 𝐹 ‘ 𝑧 ) ) )
19 breq1 ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑧 ) → ( 𝑢 𝐺 𝑤 ↔ ( 𝐹 ‘ 𝑧 ) 𝐺 𝑤 ) )
20 18 19 anbi12d ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑧 ) → ( ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) ↔ ( 𝑧 𝐹 ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) 𝐺 𝑤 ) ) )
21 17 20 ceqsexv ⊢ ( ∃ 𝑢 ( 𝑢 = ( 𝐹 ‘ 𝑧 ) ∧ ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) ) ↔ ( 𝑧 𝐹 ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) 𝐺 𝑤 ) )
22 funfvbrb ⊢ ( Fun 𝐹 → ( 𝑧 ∈ dom 𝐹 ↔ 𝑧 𝐹 ( 𝐹 ‘ 𝑧 ) ) )
23 8 22 syl ⊢ ( 𝜑 → ( 𝑧 ∈ dom 𝐹 ↔ 𝑧 𝐹 ( 𝐹 ‘ 𝑧 ) ) )
24 7 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
25 24 eleq2d ⊢ ( 𝜑 → ( 𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝐴 ) )
26 23 25 bitr3d ⊢ ( 𝜑 → ( 𝑧 𝐹 ( 𝐹 ‘ 𝑧 ) ↔ 𝑧 ∈ 𝐴 ) )
27 2 fveq1d ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) )
28 eqidd ⊢ ( 𝜑 → 𝑤 = 𝑤 )
29 27 3 28 breq123d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑧 ) 𝐺 𝑤 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ) )
30 26 29 anbi12d ⊢ ( 𝜑 → ( ( 𝑧 𝐹 ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) 𝐺 𝑤 ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ) ) )
31 nfcv ⊢ Ⅎ 𝑥 𝑧
32 nfv ⊢ Ⅎ 𝑥 𝜑
33 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 )
34 nfcv ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐵 ↦ 𝑆 )
35 nfcv ⊢ Ⅎ 𝑥 𝑤
36 33 34 35 nfbr ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤
37 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝑇
38 37 nfeq2 ⊢ Ⅎ 𝑥 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇
39 36 38 nfbi ⊢ Ⅎ 𝑥 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 )
40 32 39 nfim ⊢ Ⅎ 𝑥 ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) )
41 fveq2 ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) )
42 41 breq1d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ) )
43 csbeq1a ⊢ ( 𝑥 = 𝑧 → 𝑇 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 )
44 43 eqeq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑤 = 𝑇 ↔ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) )
45 42 44 bibi12d ⊢ ( 𝑥 = 𝑧 → ( ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = 𝑇 ) ↔ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) ) )
46 45 imbi2d ⊢ ( 𝑥 = 𝑧 → ( ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = 𝑇 ) ) ↔ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) ) ) )
47 vex ⊢ 𝑤 ∈ V
48 simpl ⊢ ( ( 𝑦 = 𝑅 ∧ 𝑢 = 𝑤 ) → 𝑦 = 𝑅 )
49 48 eleq1d ⊢ ( ( 𝑦 = 𝑅 ∧ 𝑢 = 𝑤 ) → ( 𝑦 ∈ 𝐵 ↔ 𝑅 ∈ 𝐵 ) )
50 id ⊢ ( 𝑢 = 𝑤 → 𝑢 = 𝑤 )
51 50 4 eqeqan12rd ⊢ ( ( 𝑦 = 𝑅 ∧ 𝑢 = 𝑤 ) → ( 𝑢 = 𝑆 ↔ 𝑤 = 𝑇 ) )
52 49 51 anbi12d ⊢ ( ( 𝑦 = 𝑅 ∧ 𝑢 = 𝑤 ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑢 = 𝑆 ) ↔ ( 𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇 ) ) )
53 df-mpt ⊢ ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) = { ⟨ 𝑦 , 𝑢 ⟩ ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑢 = 𝑆 ) }
54 52 53 brabga ⊢ ( ( 𝑅 ∈ 𝐵 ∧ 𝑤 ∈ V ) → ( 𝑅 ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ ( 𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇 ) ) )
55 1 47 54 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅 ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ ( 𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇 ) ) )
56 id ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴 )
57 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑅 )
58 57 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑅 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) = 𝑅 )
59 56 1 58 syl2an2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) = 𝑅 )
60 59 breq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑅 ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ) )
61 1 biantrurd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑤 = 𝑇 ↔ ( 𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇 ) ) )
62 55 60 61 3bitr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = 𝑇 ) )
63 62 expcom ⊢ ( 𝑥 ∈ 𝐴 → ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = 𝑇 ) ) )
64 31 40 46 63 vtoclgaf ⊢ ( 𝑧 ∈ 𝐴 → ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) ) )
65 64 impcom ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) )
66 65 pm5.32da ⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) ) )
67 30 66 bitrd ⊢ ( 𝜑 → ( ( 𝑧 𝐹 ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) 𝐺 𝑤 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) ) )
68 21 67 bitrid ⊢ ( 𝜑 → ( ∃ 𝑢 ( 𝑢 = ( 𝐹 ‘ 𝑧 ) ∧ ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) ) )
69 16 68 bitrd ⊢ ( 𝜑 → ( ∃ 𝑢 ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) ) )
70 vex ⊢ 𝑧 ∈ V
71 70 47 opelco ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐺 ∘ 𝐹 ) ↔ ∃ 𝑢 ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) )
72 df-mpt ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) = { ⟨ 𝑥 , 𝑣 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇 ) }
73 72 eleq2i ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑣 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇 ) } )
74 nfv ⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴
75 37 nfeq2 ⊢ Ⅎ 𝑥 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇
76 74 75 nfan ⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 )
77 nfv ⊢ Ⅎ 𝑣 ( 𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 )
78 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
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 ⊢ ( 𝜑 → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐺 ∘ 𝐹 ) ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) ) )
86 5 6 85 eqrelrdv ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) )