Theorem fmptcof2 31882

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.)

Hypotheses

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

Assertion

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

Distinct variable groups:   𝑥,𝑦   𝑦,𝐵   𝑦,𝑅

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

Proof of Theorem fmptcof2

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

Step	Hyp	Ref	Expression
1		relco 6108	. 2 ⊢ Rel (𝐺 ∘ 𝐹)
2		mptrel 5826	. 2 ⊢ Rel (𝑥 ∈ 𝐴 ↦ 𝑇)
3		fmptcof2.3	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥𝜑
4		fmptcof2.1	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥𝐴
5		fmptcof2.2	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥𝐵
6		fmptcof2.4	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵)
7	6	r19.21bi 3249	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝐵)
8		eqid 2733	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅)
9	3, 4, 5, 7, 8	fmptdF 31881	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶𝐵)
10		fmptcof2.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅))
11	10	feq1d 6703	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶𝐵))
12	9, 11	mpbird 257	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
13	12	ffund 6722	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝐹)
14		funbrfv 6943	. . . . . . . . . . 11 ⊢ (Fun 𝐹 → (𝑧𝐹𝑢 → (𝐹‘𝑧) = 𝑢))
15	14	imp 408	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ 𝑧𝐹𝑢) → (𝐹‘𝑧) = 𝑢)
16	13, 15	sylan 581	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → (𝐹‘𝑧) = 𝑢)
17	16	eqcomd 2739	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → 𝑢 = (𝐹‘𝑧))
18	17	a1d 25	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧𝐹𝑢) → (𝑢𝐺𝑤 → 𝑢 = (𝐹‘𝑧)))
19	18	expimpd 455	. . . . . 6 ⊢ (𝜑 → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) → 𝑢 = (𝐹‘𝑧)))
20	19	pm4.71rd 564	. . . . 5 ⊢ (𝜑 → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤))))
21	20	exbidv 1925	. . . 4 ⊢ (𝜑 → (∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ ∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤))))
22		fvex 6905	. . . . . 6 ⊢ (𝐹‘𝑧) ∈ V
23		breq2 5153	. . . . . . 7 ⊢ (𝑢 = (𝐹‘𝑧) → (𝑧𝐹𝑢 ↔ 𝑧𝐹(𝐹‘𝑧)))
24		breq1 5152	. . . . . . 7 ⊢ (𝑢 = (𝐹‘𝑧) → (𝑢𝐺𝑤 ↔ (𝐹‘𝑧)𝐺𝑤))
25	23, 24	anbi12d 632	. . . . . 6 ⊢ (𝑢 = (𝐹‘𝑧) → ((𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤)))
26	22, 25	ceqsexv 3526	. . . . 5 ⊢ (∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) ↔ (𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤))
27		funfvbrb 7053	. . . . . . . . 9 ⊢ (Fun 𝐹 → (𝑧 ∈ dom 𝐹 ↔ 𝑧𝐹(𝐹‘𝑧)))
28	13, 27	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑧 ∈ dom 𝐹 ↔ 𝑧𝐹(𝐹‘𝑧)))
29	12	fdmd 6729	. . . . . . . . 9 ⊢ (𝜑 → dom 𝐹 = 𝐴)
30	29	eleq2d 2820	. . . . . . . 8 ⊢ (𝜑 → (𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝐴))
31	28, 30	bitr3d 281	. . . . . . 7 ⊢ (𝜑 → (𝑧𝐹(𝐹‘𝑧) ↔ 𝑧 ∈ 𝐴))
32	10	fveq1d 6894	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝑧) = ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧))
33		fmptcof2.6	. . . . . . . 8 ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆))
34		eqidd 2734	. . . . . . . 8 ⊢ (𝜑 → 𝑤 = 𝑤)
35	32, 33, 34	breq123d 5163	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘𝑧)𝐺𝑤 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤))
36	31, 35	anbi12d 632	. . . . . 6 ⊢ (𝜑 → ((𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤)))
37	4	nfcri 2891	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐴
38		nffvmpt1 6903	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)
39		fmptcof2.x	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥𝑆
40	5, 39	nfmpt 5256	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐵 ↦ 𝑆)
41		nfcv 2904	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥𝑤
42	38, 40, 41	nfbr 5196	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤
43		nfcsb1v 3919	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝑇
44	43	nfeq2 2921	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑤 = ⦋𝑧 / 𝑥⦌𝑇
45	42, 44	nfbi 1907	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)
46	3, 45	nfim 1900	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
47	37, 46	nfim 1900	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑧 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
48		eleq1w 2817	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))
49		fveq2 6892	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧))
50	49	breq1d 5159	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤))
51		csbeq1a 3908	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → 𝑇 = ⦋𝑧 / 𝑥⦌𝑇)
52	51	eqeq2d 2744	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝑤 = 𝑇 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
53	50, 52	bibi12d 346	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇) ↔ (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
54	53	imbi2d 341	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → ((𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇)) ↔ (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))))
55	48, 54	imbi12d 345	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇))) ↔ (𝑧 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))))
56		vex 3479	. . . . . . . . . . . 12 ⊢ 𝑤 ∈ V
57		nfv 1918	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦 𝑅 ∈ 𝐵
58		fmptcof2.y	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦𝑇
59	58	nfeq2 2921	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦 𝑤 = 𝑇
60	57, 59	nfan 1903	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)
61		simpl 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → 𝑦 = 𝑅)
62	61	eleq1d 2819	. . . . . . . . . . . . . 14 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → (𝑦 ∈ 𝐵 ↔ 𝑅 ∈ 𝐵))
63		simpr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → 𝑢 = 𝑤)
64		fmptcof2.7	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇)
65	64	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → 𝑆 = 𝑇)
66	63, 65	eqeq12d 2749	. . . . . . . . . . . . . 14 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → (𝑢 = 𝑆 ↔ 𝑤 = 𝑇))
67	62, 66	anbi12d 632	. . . . . . . . . . . . 13 ⊢ ((𝑦 = 𝑅 ∧ 𝑢 = 𝑤) → ((𝑦 ∈ 𝐵 ∧ 𝑢 = 𝑆) ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
68		df-mpt 5233	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐵 ↦ 𝑆) = {⟨𝑦, 𝑢⟩ ∣ (𝑦 ∈ 𝐵 ∧ 𝑢 = 𝑆)}
69	60, 67, 68	brabgaf 31837	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ 𝐵 ∧ 𝑤 ∈ V) → (𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
70	7, 56, 69	sylancl 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
71		simpr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
72	4	fvmpt2f 7000	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑅 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅)
73	71, 7, 72	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅)
74	73	breq1d 5159	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑅(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤))
75	7	biantrurd 534	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑤 = 𝑇 ↔ (𝑅 ∈ 𝐵 ∧ 𝑤 = 𝑇)))
76	70, 74, 75	3bitr4d 311	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇))
77	76	expcom 415	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = 𝑇)))
78	47, 55, 77	chvarfv 2234	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐴 → (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
79	78	impcom 409	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
80	79	pm5.32da 580	. . . . . 6 ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑧)(𝑦 ∈ 𝐵 ↦ 𝑆)𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
81	36, 80	bitrd 279	. . . . 5 ⊢ (𝜑 → ((𝑧𝐹(𝐹‘𝑧) ∧ (𝐹‘𝑧)𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
82	26, 81	bitrid 283	. . . 4 ⊢ (𝜑 → (∃𝑢(𝑢 = (𝐹‘𝑧) ∧ (𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤)) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
83	21, 82	bitrd 279	. . 3 ⊢ (𝜑 → (∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
84		vex 3479	. . . 4 ⊢ 𝑧 ∈ V
85	84, 56	opelco 5872	. . 3 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝐺 ∘ 𝐹) ↔ ∃𝑢(𝑧𝐹𝑢 ∧ 𝑢𝐺𝑤))
86		df-mpt 5233	. . . . 5 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑇) = {⟨𝑥, 𝑣⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)}
87	86	eleq2i 2826	. . . 4 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝑥 ∈ 𝐴 ↦ 𝑇) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)})
88	43	nfeq2 2921	. . . . . 6 ⊢ Ⅎ𝑥 𝑣 = ⦋𝑧 / 𝑥⦌𝑇
89	37, 88	nfan 1903	. . . . 5 ⊢ Ⅎ𝑥(𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇)
90		nfv 1918	. . . . 5 ⊢ Ⅎ𝑣(𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)
91	51	eqeq2d 2744	. . . . . 6 ⊢ (𝑥 = 𝑧 → (𝑣 = 𝑇 ↔ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇))
92	48, 91	anbi12d 632	. . . . 5 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇)))
93		eqeq1 2737	. . . . . 6 ⊢ (𝑣 = 𝑤 → (𝑣 = ⦋𝑧 / 𝑥⦌𝑇 ↔ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
94	93	anbi2d 630	. . . . 5 ⊢ (𝑣 = 𝑤 → ((𝑧 ∈ 𝐴 ∧ 𝑣 = ⦋𝑧 / 𝑥⦌𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇)))
95	89, 90, 84, 56, 92, 94	opelopabf 5546	. . . 4 ⊢ (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑣 = 𝑇)} ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
96	87, 95	bitri 275	. . 3 ⊢ (⟨𝑧, 𝑤⟩ ∈ (𝑥 ∈ 𝐴 ↦ 𝑇) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋𝑧 / 𝑥⦌𝑇))
97	83, 85, 96	3bitr4g 314	. 2 ⊢ (𝜑 → (⟨𝑧, 𝑤⟩ ∈ (𝐺 ∘ 𝐹) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑥 ∈ 𝐴 ↦ 𝑇)))
98	1, 2, 97	eqrelrdv 5793	1 ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542  ∃wex 1782  Ⅎwnf 1786   ∈ wcel 2107  Ⅎwnfc 2884  ∀wral 3062  Vcvv 3475  ⦋csb 3894  ⟨cop 4635   class class class wbr 5149  {copab 5211   ↦ cmpt 5232  dom cdm 5677   ∘ ccom 5681  Fun wfun 6538  ⟶wf 6540  ‘cfv 6544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552

This theorem is referenced by:  esumf1o  33048