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	syl5bb	⊢ ( 𝜑 → ( ∃ 𝑢 ( 𝑢 = ( 𝐹 ‘ 𝑧 ) ∧ ( 𝑧 𝐹 𝑢 ∧ 𝑢 𝐺 𝑤 ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑤 = ⦋ 𝑧 / 𝑥 ⦌ 𝑇 ) ) )
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	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) )