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	fmptdf2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ 𝐵 )
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	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) )