Theorem fmptco 5351

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

Hypotheses

Ref	Expression
fmptco.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝐵)
fmptco.2	⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅))
fmptco.3	⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆))
fmptco.4	⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇)

Assertion

Ref	Expression
fmptco	⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇))

Distinct variable groups:   𝑥,𝐴   𝑥,𝑦,𝐵   𝑦,𝑅   𝜑,𝑥   𝑥,𝑆   𝑦,𝑇

Allowed substitution hints:   𝜑(𝑦)   𝐴(𝑦)   𝑅(𝑥)   𝑆(𝑦)   𝑇(𝑥)   𝐹(𝑥,𝑦)   𝐺(𝑥,𝑦)

Proof of Theorem fmptco

Dummy variables 𝑣 𝑢 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relco 4839	. 2 ⊢ Rel (𝐺 ∘ 𝐹)
2		funmpt 4958	. . 3 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝑇)
3		funrel 4939	. . 3 ⊢ (Fun (𝑥 ∈ 𝐴 ↦ 𝑇) → Rel (𝑥 ∈ 𝐴 ↦ 𝑇))
4	2, 3	ax-mp 7	. 2 ⊢ Rel (𝑥 ∈ 𝐴 ↦ 𝑇)
5		fmptco.1	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝐵)
6		eqid 2081	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅)
7	5, 6	fmptd 5343	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶𝐵)
8		fmptco.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅))
9	8	feq1d 5054	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶𝐵))
10	7, 9	mpbird 165	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
11		ffun 5068	. . . . . . . . . . 11 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹)
12	10, 11	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝐹)
13		funbrfv 5233	. . . . . . . . . . 11 ⊢ (Fun 𝐹 → (𝑧𝐹𝑢 → (𝐹‘𝑧) = 𝑢))
14	13	imp 122	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ 𝑧𝐹𝑢) → (𝐹‘𝑧) = 𝑢)
15	12, 14	sylan 277	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → (𝐹‘𝑧) = 𝑢)
16	15	eqcomd 2086	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → 𝑢 = (𝐹‘𝑧))
17	16	a1d 22	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → (𝑢𝐺𝑤 → 𝑢 = (𝐹‘𝑧)))
18	17	expimpd 355	. . . . . 6 ⊢ (𝜑 → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) → 𝑢 = (𝐹‘𝑧)))
19	18	pm4.71rd 386	. . . . 5 ⊢ (𝜑 → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤))))
20	19	exbidv 1746	. . . 4 ⊢ (𝜑 → (∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ ∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤))))
21		exsimpl 1548	. . . . . . 7 ⊢ (∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) → ∃𝑢 𝑢 = (𝐹‘𝑧))
22		isset 2605	. . . . . . 7 ⊢ ((𝐹‘𝑧) ∈ V ↔ ∃𝑢 𝑢 = (𝐹‘𝑧))
23	21, 22	sylibr 132	. . . . . 6 ⊢ (∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) → (𝐹‘𝑧) ∈ V)
24	23	a1i 9	. . . . 5 ⊢ (𝜑 → (∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) → (𝐹‘𝑧) ∈ V))
25	12	adantr 270	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → Fun 𝐹)
26		fdm 5070	. . . . . . . . . . 11 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)
27	10, 26	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → dom 𝐹 = 𝐴)
28	27	eleq2d 2148	. . . . . . . . 9 ⊢ (𝜑 → (𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝐴))
29	28	biimpar 291	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ dom 𝐹)
30		funfvex 5212	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹) → (𝐹‘𝑧) ∈ V)
31	25, 29, 30	syl2anc 403	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ V)
32	31	adantrr 462	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)) → (𝐹‘𝑧) ∈ V)
33	32	ex 113	. . . . 5 ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇) → (𝐹‘𝑧) ∈ V))
34		breq2 3789	. . . . . . . . 9 ⊢ (𝑢 = (𝐹‘𝑧) → (𝑧𝐹𝑢 ↔ 𝑧𝐹(𝐹‘𝑧)))
35		breq1 3788	. . . . . . . . 9 ⊢ (𝑢 = (𝐹‘𝑧) → (𝑢𝐺𝑤 ↔ (𝐹‘𝑧)𝐺𝑤))
36	34, 35	anbi12d 456	. . . . . . . 8 ⊢ (𝑢 = (𝐹‘𝑧) → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤)))
37	36	ceqsexgv 2724	. . . . . . 7 ⊢ ((𝐹‘𝑧) ∈ V → (∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) ↔ (𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤)))
38		funfvbrb 5301	. . . . . . . . . . 11 ⊢ (Fun 𝐹 → (𝑧 ∈ dom 𝐹 ↔ 𝑧𝐹(𝐹‘𝑧)))
39	12, 38	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ dom 𝐹 ↔ 𝑧𝐹(𝐹‘𝑧)))
40	39, 28	bitr3d 188	. . . . . . . . 9 ⊢ (𝜑 → (𝑧𝐹(𝐹‘𝑧) ↔ 𝑧 ∈ 𝐴))
41	8	fveq1d 5200	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘𝑧) = ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧))
42		fmptco.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆))
43		eqidd 2082	. . . . . . . . . 10 ⊢ (𝜑 → 𝑤 = 𝑤)
44	41, 42, 43	breq123d 3799	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘𝑧)𝐺𝑤 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤))
45	40, 44	anbi12d 456	. . . . . . . 8 ⊢ (𝜑 → ((𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤)))
46		nfcv 2219	. . . . . . . . . . 11 ⊢ Ⅎ𝑥𝑧
47		nfv 1461	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝜑
48		nffvmpt1 5206	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)
49		nfcv 2219	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐵 ↦ 𝑆)
50		nfcv 2219	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥𝑤
51	48, 49, 50	nfbr 3829	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤
52		nfcsb1v 2938	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝑇
53	52	nfeq2 2230	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥 𝑤 = ⦋𝑧 / 𝑥⦌𝑇
54	51, 53	nfbi 1521	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)
55	47, 54	nfim 1504	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
56		fveq2 5198	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧))
57	56	breq1d 3795	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤))
58		csbeq1a 2916	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → 𝑇 = ⦋𝑧 / 𝑥⦌𝑇)
59	58	eqeq2d 2092	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑤 = 𝑇 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
60	57, 59	bibi12d 233	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇) ↔ (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
61	60	imbi2d 228	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇)) ↔ (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))))
62		vex 2604	. . . . . . . . . . . . . 14 ⊢ 𝑤 ∈ V
63		simpl 107	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → 𝑦 = 𝑅)
64	63	eleq1d 2147	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → (𝑦 ∈ 𝐵 ↔ 𝑅 ∈ 𝐵))
65		simpr 108	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → 𝑢 = 𝑤)
66		fmptco.4	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇)
67	66	adantr 270	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → 𝑆 = 𝑇)
68	65, 67	eqeq12d 2095	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → (𝑢 = 𝑆 ↔ 𝑤 = 𝑇))
69	64, 68	anbi12d 456	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → ((𝑦 ∈ 𝐵 ∧ 𝑢 = 𝑆) ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
70		df-mpt 3841	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝐵 ↦ 𝑆) = {⟨𝑦, 𝑢⟩ ∣ (𝑦 ∈ 𝐵 ∧ 𝑢 = 𝑆)}
71	69, 70	brabga 4019	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ 𝐵 ∧ 𝑤 ∈ V) → (𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
72	5, 62, 71	sylancl 404	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
73		simpr 108	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
74	6	fvmpt2 5275	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑅 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅)
75	73, 5, 74	syl2anc 403	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅)
76	75	breq1d 3795	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤))
77	5	biantrurd 299	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑤 = 𝑇 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
78	72, 76, 77	3bitr4d 218	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇))
79	78	expcom 114	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇)))
80	46, 55, 61, 79	vtoclgaf 2663	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
81	80	impcom 123	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
82	81	pm5.32da 439	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
83	45, 82	bitrd 186	. . . . . . 7 ⊢ (𝜑 → ((𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
84	37, 83	sylan9bbr 450	. . . . . 6 ⊢ ((𝜑 ∧ (𝐹‘𝑧) ∈ V) → (∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
85	84	ex 113	. . . . 5 ⊢ (𝜑 → ((𝐹‘𝑧) ∈ V → (∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))))
86	24, 33, 85	pm5.21ndd 653	. . . 4 ⊢ (𝜑 → (∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
87	20, 86	bitrd 186	. . 3 ⊢ (𝜑 → (∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
88		vex 2604	. . . 4 ⊢ 𝑧 ∈ V
89	88, 62	opelco 4525	. . 3 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝐺 ∘ 𝐹) ↔ ∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤))
90		df-mpt 3841	. . . . 5 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑇) = {⟨𝑥, 𝑣⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)}
91	90	eleq2i 2145	. . . 4 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝑥 ∈ 𝐴 ↦ 𝑇) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)})
92		nfv 1461	. . . . . 6 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐴
93	52	nfeq2 2230	. . . . . 6 ⊢ Ⅎ𝑥 𝑣 = ⦋𝑧 / 𝑥⦌𝑇
94	92, 93	nfan 1497	. . . . 5 ⊢ Ⅎ𝑥(𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇)
95		nfv 1461	. . . . 5 ⊢ Ⅎ𝑣(𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)
96		eleq1 2141	. . . . . 6 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))
97	58	eqeq2d 2092	. . . . . 6 ⊢ (𝑥 = 𝑧 → (𝑣 = 𝑇 ↔ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇))
98	96, 97	anbi12d 456	. . . . 5 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇)))
99		eqeq1 2087	. . . . . 6 ⊢ (𝑣 = 𝑤 → (𝑣 = ⦋𝑧 / 𝑥⦌𝑇 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
100	99	anbi2d 451	. . . . 5 ⊢ (𝑣 = 𝑤 → ((𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
101	94, 95, 88, 62, 98, 100	opelopabf 4029	. . . 4 ⊢ (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)} ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
102	91, 101	bitri 182	. . 3 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝑥 ∈ 𝐴 ↦ 𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
103	87, 89, 102	3bitr4g 221	. 2 ⊢ (𝜑 → (⟨𝑧, 𝑤⟩ ∈ (𝐺 ∘ 𝐹) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑥 ∈ 𝐴 ↦ 𝑇)))
104	1, 4, 103	eqrelrdv 4454	1 ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇))

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103   = wceq 1284  ∃wex 1421   ∈ wcel 1433  Vcvv 2601  ⦋csb 2908  ⟨cop 3401   class class class wbr 3785  {copab 3838   ↦ cmpt 3839  dom cdm 4363   ∘ ccom 4367  Rel wrel 4368  Fun wfun 4916  ⟶wf 4918  ‘cfv 4922

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-sep 3896  ax-pow 3948  ax-pr 3964

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-eu 1944  df-mo 1945  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ral 2353  df-rex 2354  df-rab 2357  df-v 2603  df-sbc 2816  df-csb 2909  df-un 2977  df-in 2979  df-ss 2986  df-pw 3384  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-br 3786  df-opab 3840  df-mpt 3841  df-id 4048  df-xp 4369  df-rel 4370  df-cnv 4371  df-co 4372  df-dm 4373  df-rn 4374  df-res 4375  df-ima 4376  df-iota 4887  df-fun 4924  df-fn 4925  df-f 4926  df-fv 4930

This theorem is referenced by:  fmptcof  5352  fcompt  5354  fcoconst  5355  ofco  5749