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

Metamath Proof Explorer

Theorem fmptcof2

Description: Composition of two functions expressed as ordered-pair class abstractions. (Contributed by FL, 21-Jun-2012) (Revised by Mario Carneiro, 24-Jul-2014) (Revised by Thierry Arnoux, 10-May-2017)

Ref Expression
Hypotheses fmptcof2.x ⊢ Ⅎ 𝑥 𝑆
fmptcof2.y ⊢ Ⅎ 𝑦 𝑇
fmptcof2.1 ⊢ Ⅎ 𝑥 𝐴
fmptcof2.2 ⊢ Ⅎ 𝑥 𝐵
fmptcof2.3 ⊢ Ⅎ 𝑥 𝜑
fmptcof2.4 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑅 ∈ 𝐵 )
fmptcof2.5 ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) )
fmptcof2.6 ⊢ ( 𝜑 → 𝐺 = ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) )
fmptcof2.7 ⊢ ( 𝑦 = 𝑅 → 𝑆 = 𝑇 )
Assertion fmptcof2 ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 fmptcof2.x ⊢ Ⅎ 𝑥 𝑆
2 fmptcof2.y ⊢ Ⅎ 𝑦 𝑇
3 fmptcof2.1 ⊢ Ⅎ 𝑥 𝐴
4 fmptcof2.2 ⊢ Ⅎ 𝑥 𝐵
5 fmptcof2.3 ⊢ Ⅎ 𝑥 𝜑
6 fmptcof2.4 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑅 ∈ 𝐵 )
7 fmptcof2.5 ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) )
8 fmptcof2.6 ⊢ ( 𝜑 → 𝐺 = ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) )
9 fmptcof2.7 ⊢ ( 𝑦 = 𝑅 → 𝑆 = 𝑇 )
10 relco ⊢ Rel ( 𝐺 ∘ 𝐹 )
11 mptrel ⊢ Rel ( 𝑥 ∈ 𝐴 ↦ 𝑇 )
12 6 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑅 ∈ 𝐵 )
13 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑅 )
14 5 3 4 12 13 fmptdF ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ 𝐵 )
15 7 feq1d ⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ 𝐵 ) )
16 14 15 mpbird ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
17 16 ffund ⊢ ( 𝜑 → Fun 𝐹 )
18 funbrfv ⊢ ( Fun 𝐹 → ( 𝑧 𝐹 𝑢 → ( 𝐹 ‘ 𝑧 ) = 𝑢 ) )
19 18 imp ⊢ ( ( Fun 𝐹 ∧ 𝑧 𝐹 𝑢 ) → ( 𝐹 ‘ 𝑧 ) = 𝑢 )
20 17 19 sylan ⊢ ( ( 𝜑 ∧ 𝑧 𝐹 𝑢 ) → ( 𝐹 ‘ 𝑧 ) = 𝑢 )
21 20 eqcomd ⊢ ( ( 𝜑 ∧ 𝑧 𝐹 𝑢 ) → 𝑢 = ( 𝐹 ‘ 𝑧 ) )
22 21 a1d ⊢ ( ( 𝜑 ∧ 𝑧 𝐹 𝑢 ) → ( 𝑢 𝐺 𝑤 → 𝑢 = ( 𝐹 ‘ 𝑧 ) ) )
23 22 expimpd ⊢ ( 𝜑 → ( ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) → 𝑢 = ( 𝐹 ‘ 𝑧 ) ) )
24 23 pm4.71rd ⊢ ( 𝜑 → ( ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) ↔ ( 𝑢 = ( 𝐹 ‘ 𝑧 ) ∧ ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) ) ) )
25 24 exbidv ⊢ ( 𝜑 → ( ∃ 𝑢 ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) ↔ ∃ 𝑢 ( 𝑢 = ( 𝐹 ‘ 𝑧 ) ∧ ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) ) ) )
26 fvex ⊢ ( 𝐹 ‘ 𝑧 ) ∈ V
27 breq2 ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑧 ) → ( 𝑧 𝐹 𝑢 ↔ 𝑧 𝐹 ( 𝐹 ‘ 𝑧 ) ) )
28 breq1 ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑧 ) → ( 𝑢 𝐺 𝑤 ↔ ( 𝐹 ‘ 𝑧 ) 𝐺 𝑤 ) )
29 27 28 anbi12d ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑧 ) → ( ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) ↔ ( 𝑧 𝐹 ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) 𝐺 𝑤 ) ) )
30 26 29 ceqsexv ⊢ ( ∃ 𝑢 ( 𝑢 = ( 𝐹 ‘ 𝑧 ) ∧ ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) ) ↔ ( 𝑧 𝐹 ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) 𝐺 𝑤 ) )
31 funfvbrb ⊢ ( Fun 𝐹 → ( 𝑧 ∈ dom 𝐹 ↔ 𝑧 𝐹 ( 𝐹 ‘ 𝑧 ) ) )
32 17 31 syl ⊢ ( 𝜑 → ( 𝑧 ∈ dom 𝐹 ↔ 𝑧 𝐹 ( 𝐹 ‘ 𝑧 ) ) )
33 16 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
34 33 eleq2d ⊢ ( 𝜑 → ( 𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝐴 ) )
35 32 34 bitr3d ⊢ ( 𝜑 → ( 𝑧 𝐹 ( 𝐹 ‘ 𝑧 ) ↔ 𝑧 ∈ 𝐴 ) )
36 7 fveq1d ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) )
37 eqidd ⊢ ( 𝜑 → 𝑤 = 𝑤 )
38 36 8 37 breq123d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑧 ) 𝐺 𝑤 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ) )
39 35 38 anbi12d ⊢ ( 𝜑 → ( ( 𝑧 𝐹 ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) 𝐺 𝑤 ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ) ) )
40 3 nfcri ⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴
41 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 )
42 4 1 nfmpt ⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐵 ↦ 𝑆 )
43 nfcv ⊢ Ⅎ 𝑥 𝑤
44 41 42 43 nfbr ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤
45 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝑇
46 45 nfeq2 ⊢ Ⅎ 𝑥 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇
47 44 46 nfbi ⊢ Ⅎ 𝑥 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 )
48 5 47 nfim ⊢ Ⅎ 𝑥 ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) )
49 40 48 nfim ⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝐴 → ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) ) )
50 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
51 fveq2 ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) )
52 51 breq1d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ) )
53 csbeq1a ⊢ ( 𝑥 = 𝑧 → 𝑇 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 )
54 53 eqeq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑤 = 𝑇 ↔ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) )
55 52 54 bibi12d ⊢ ( 𝑥 = 𝑧 → ( ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = 𝑇 ) ↔ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) ) )
56 55 imbi2d ⊢ ( 𝑥 = 𝑧 → ( ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = 𝑇 ) ) ↔ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) ) ) )
57 50 56 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 → ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = 𝑇 ) ) ) ↔ ( 𝑧 ∈ 𝐴 → ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) ) ) ) )
58 vex ⊢ 𝑤 ∈ V
59 nfv ⊢ Ⅎ 𝑦 𝑅 ∈ 𝐵
60 2 nfeq2 ⊢ Ⅎ 𝑦 𝑤 = 𝑇
61 59 60 nfan ⊢ Ⅎ 𝑦 ( 𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇 )
62 simpl ⊢ ( ( 𝑦 = 𝑅 ∧ 𝑢 = 𝑤 ) → 𝑦 = 𝑅 )
63 62 eleq1d ⊢ ( ( 𝑦 = 𝑅 ∧ 𝑢 = 𝑤 ) → ( 𝑦 ∈ 𝐵 ↔ 𝑅 ∈ 𝐵 ) )
64 simpr ⊢ ( ( 𝑦 = 𝑅 ∧ 𝑢 = 𝑤 ) → 𝑢 = 𝑤 )
65 9 adantr ⊢ ( ( 𝑦 = 𝑅 ∧ 𝑢 = 𝑤 ) → 𝑆 = 𝑇 )
66 64 65 eqeq12d ⊢ ( ( 𝑦 = 𝑅 ∧ 𝑢 = 𝑤 ) → ( 𝑢 = 𝑆 ↔ 𝑤 = 𝑇 ) )
67 63 66 anbi12d ⊢ ( ( 𝑦 = 𝑅 ∧ 𝑢 = 𝑤 ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑢 = 𝑆 ) ↔ ( 𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇 ) ) )
68 df-mpt ⊢ ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) = { ⟨ 𝑦 , 𝑢 ⟩ ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑢 = 𝑆 ) }
69 61 67 68 brabgaf ⊢ ( ( 𝑅 ∈ 𝐵 ∧ 𝑤 ∈ V ) → ( 𝑅 ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ ( 𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇 ) ) )
70 12 58 69 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅 ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ ( 𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇 ) ) )
71 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
72 3 fvmpt2f ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑅 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) = 𝑅 )
73 71 12 72 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) = 𝑅 )
74 73 breq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑅 ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ) )
75 12 biantrurd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑤 = 𝑇 ↔ ( 𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇 ) ) )
76 70 74 75 3bitr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = 𝑇 ) )
77 76 expcom ⊢ ( 𝑥 ∈ 𝐴 → ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑥 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = 𝑇 ) ) )
78 49 57 77 chvarfv ⊢ ( 𝑧 ∈ 𝐴 → ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) ) )
79 78 impcom ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ↔ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) )
80 79 pm5.32da ⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ 𝑧 ) ( 𝑦 ∈ 𝐵 ↦ 𝑆 ) 𝑤 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) ) )
81 39 80 bitrd ⊢ ( 𝜑 → ( ( 𝑧 𝐹 ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) 𝐺 𝑤 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) ) )
82 30 81 bitrid ⊢ ( 𝜑 → ( ∃ 𝑢 ( 𝑢 = ( 𝐹 ‘ 𝑧 ) ∧ ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) ) )
83 25 82 bitrd ⊢ ( 𝜑 → ( ∃ 𝑢 ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) ) )
84 vex ⊢ 𝑧 ∈ V
85 84 58 opelco ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐺 ∘ 𝐹 ) ↔ ∃ 𝑢 ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) )
86 df-mpt ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) = { ⟨ 𝑥 , 𝑣 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇 ) }
87 86 eleq2i ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑣 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇 ) } )
88 45 nfeq2 ⊢ Ⅎ 𝑥 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇
89 40 88 nfan ⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 )
90 nfv ⊢ Ⅎ 𝑣 ( 𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 )
91 53 eqeq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑣 = 𝑇 ↔ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) )
92 50 91 anbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) ) )
93 eqeq1 ⊢ ( 𝑣 = 𝑤 → ( 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ↔ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) )
94 93 anbi2d ⊢ ( 𝑣 = 𝑤 → ( ( 𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) ) )
95 89 90 84 58 92 94 opelopabf ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑣 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇 ) } ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) )
96 87 95 bitri ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) )
97 83 85 96 3bitr4g ⊢ ( 𝜑 → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐺 ∘ 𝐹 ) ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) ) )
98 10 11 97 eqrelrdv ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) )