uncfcurf

Description: Cancellation of uncurry with curry. (Contributed by Mario Carneiro, 13-Jan-2017)

	Ref	Expression
Hypotheses	uncfcurf.g	⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F 𝐹 )
	uncfcurf.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	uncfcurf.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	uncfcurf.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
Assertion	uncfcurf	⊢ ( 𝜑 → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		uncfcurf.g	⊢ 𝐺 = ( ⟨ 𝐶 , 𝐷 ⟩ curry_F 𝐹 )
2		uncfcurf.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		uncfcurf.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
4		uncfcurf.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
5		eqid	⊢ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) = ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 )
6	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝐷 ∈ Cat )
7		funcrcl	⊢ ( 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) → ( ( 𝐶 ×_c 𝐷 ) ∈ Cat ∧ 𝐸 ∈ Cat ) )
8	4 7	syl	⊢ ( 𝜑 → ( ( 𝐶 ×_c 𝐷 ) ∈ Cat ∧ 𝐸 ∈ Cat ) )
9	8	simprd	⊢ ( 𝜑 → 𝐸 ∈ Cat )
10	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝐸 ∈ Cat )
11		eqid	⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
12	1 11 2 3 4	curfcl	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) )
13	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) )
14		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
15		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
16		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
17		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
18	5 6 10 13 14 15 16 17	uncf1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑥 ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) 𝑦 ) = ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) )
19	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝐶 ∈ Cat )
20	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
21		eqid	⊢ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 )
22	1 14 19 6 20 15 16 21 17	curf11	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) = ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) )
23	18 22	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑥 ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) 𝑦 ) = ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) )
24	23	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ( 𝑥 ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) 𝑦 ) = ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) )
25		eqid	⊢ ( 𝐶 ×_c 𝐷 ) = ( 𝐶 ×_c 𝐷 )
26	25 14 15	xpcbas	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( Base ‘ ( 𝐶 ×_c 𝐷 ) )
27		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
28		relfunc	⊢ Rel ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 )
29	5 3 9 12	uncfcl	⊢ ( 𝜑 → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
30		1st2ndbr	⊢ ( ( Rel ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ∧ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ) → ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) )
31	28 29 30	sylancr	⊢ ( 𝜑 → ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) )
32	26 27 31	funcf1	⊢ ( 𝜑 → ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) : ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ⟶ ( Base ‘ 𝐸 ) )
33	32	ffnd	⊢ ( 𝜑 → ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
34		1st2ndbr	⊢ ( ( Rel ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ∧ 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ) → ( 1^st ‘ 𝐹 ) ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
35	28 4 34	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
36	26 27 35	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ⟶ ( Base ‘ 𝐸 ) )
37	36	ffnd	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
38		eqfnov2	⊢ ( ( ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∧ ( 1^st ‘ 𝐹 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) → ( ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) = ( 1^st ‘ 𝐹 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ( 𝑥 ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) 𝑦 ) = ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) )
39	33 37 38	syl2anc	⊢ ( 𝜑 → ( ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) = ( 1^st ‘ 𝐹 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ( 𝑥 ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) 𝑦 ) = ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) ) )
40	24 39	mpbird	⊢ ( 𝜑 → ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) = ( 1^st ‘ 𝐹 ) )
41	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝐷 ∈ Cat )
42	9	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝐸 ∈ Cat )
43	12	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) )
44	16	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
45	44	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
46	17	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
47	46	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
48		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
49		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
50		simprl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
51	50	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
52		simprr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑤 ∈ ( Base ‘ 𝐷 ) )
53	52	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑤 ∈ ( Base ‘ 𝐷 ) )
54		simprl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) )
55		simprr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) )
56	5 41 42 43 14 15 45 47 48 49 51 53 54 55	uncf2	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) = ( ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ‘ 𝑤 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) ) ( ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑤 ) ‘ 𝑔 ) ) )
57	2	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝐶 ∈ Cat )
58	4	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) )
59	1 14 57 41 58 15 45 21 47	curf11	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) = ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) )
60		df-ov	⊢ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑦 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
61	59 60	eqtrdi	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
62	1 14 57 41 58 15 45 21 53	curf11	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) = ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑤 ) )
63		df-ov	⊢ ( 𝑥 ( 1^st ‘ 𝐹 ) 𝑤 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ )
64	62 63	eqtrdi	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) )
65	61 64	opeq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) ⟩ = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) ⟩ )
66		eqid	⊢ ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 )
67	1 14 57 41 58 15 51 66 53	curf11	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) = ( 𝑧 ( 1^st ‘ 𝐹 ) 𝑤 ) )
68		df-ov	⊢ ( 𝑧 ( 1^st ‘ 𝐹 ) 𝑤 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ )
69	67 68	eqtrdi	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) = ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) )
70	65 69	oveq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) ) = ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) )
71		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
72		eqid	⊢ ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) = ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 )
73	1 14 57 41 58 15 48 71 45 51 54 72 53	curf2val	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ‘ 𝑤 ) = ( 𝑓 ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) )
74		df-ov	⊢ ( 𝑓 ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) = ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ )
75	73 74	eqtrdi	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ‘ 𝑤 ) = ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) )
76		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
77	1 14 57 41 58 15 45 21 47 49 76 53 55	curf12	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑤 ) ‘ 𝑔 ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑤 ⟩ ) 𝑔 ) )
78		df-ov	⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑤 ⟩ ) 𝑔 ) = ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ )
79	77 78	eqtrdi	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑤 ) ‘ 𝑔 ) = ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ) )
80	70 75 79	oveq123d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ‘ 𝑤 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) ) ( ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑤 ) ‘ 𝑔 ) ) = ( ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ) ) )
81		eqid	⊢ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) = ( Hom ‘ ( 𝐶 ×_c 𝐷 ) )
82		eqid	⊢ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) = ( comp ‘ ( 𝐶 ×_c 𝐷 ) )
83		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
84	35	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( 1^st ‘ 𝐹 ) ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
85	84	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( 1^st ‘ 𝐹 ) ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
86		opelxpi	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
87	86	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
88	87	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
89	45 53	opelxpd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝑥 , 𝑤 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
90		opelxpi	⊢ ( ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
91	90	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
92	91	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
93	14 48 76 57 45	catidcl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
94	93 55	opelxpd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ∈ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
95	25 14 15 48 49 45 47 45 53 81	xpchom2	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑥 , 𝑤 ⟩ ) = ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
96	94 95	eleqtrrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ∈ ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑥 , 𝑤 ⟩ ) )
97	15 49 71 41 53	catidcl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ∈ ( 𝑤 ( Hom ‘ 𝐷 ) 𝑤 ) )
98	54 97	opelxpd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ∈ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑤 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
99	25 14 15 48 49 45 53 51 53 81	xpchom2	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ 𝑥 , 𝑤 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑤 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
100	98 99	eleqtrrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ∈ ( ⟨ 𝑥 , 𝑤 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) )
101	26 81 82 83 85 88 89 92 96 100	funcco	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ( ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ) ) = ( ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) , ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑥 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ) ) )
102		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
103		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
104	25 14 15 48 49 45 47 45 53 102 103 82 51 53 93 55 54 97	xpcco2	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ) = ⟨ ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) , ( ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ( ⟨ 𝑦 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ⟩ )
105	104	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ( ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ) ) = ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) , ( ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ( ⟨ 𝑦 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ⟩ ) )
106		df-ov	⊢ ( ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ( ⟨ 𝑦 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ) = ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) , ( ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ( ⟨ 𝑦 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ⟩ )
107	105 106	eqtr4di	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ( ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ) ) = ( ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ( ⟨ 𝑦 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ) )
108	14 48 76 57 45 102 51 54	catrid	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = 𝑓 )
109	15 49 71 41 47 103 53 55	catlid	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ( ⟨ 𝑦 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) = 𝑔 )
110	108 109	oveq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ( ⟨ 𝑦 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ) = ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) )
111	107 110	eqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ( ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑥 , 𝑤 ⟩ ⟩ ( comp ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ) ) = ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) )
112	80 101 111	3eqtr2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ‘ 𝑤 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑦 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ‘ 𝑤 ) ) ( ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑤 ) ‘ 𝑔 ) ) = ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) )
113	56 112	eqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) )
114	113	ralrimivva	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) )
115		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
116	31	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) )
117	26 81 115 116 87 91	funcf2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) : ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟶ ( ( ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) )
118	25 14 15 48 49 44 46 50 52 81	xpchom2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
119	118	feq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) : ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟶ ( ( ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) : ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ⟶ ( ( ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
120	117 119	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) : ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ⟶ ( ( ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) )
121	120	ffnd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) Fn ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
122	26 81 115 84 87 91	funcf2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) : ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) )
123	118	feq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) : ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) : ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
124	122 123	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) : ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) ) )
125	124	ffnd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) Fn ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) )
126		eqfnov2	⊢ ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) Fn ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) Fn ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) ) )
127	121 125 126	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑤 ) ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) 𝑔 ) ) )
128	114 127	mpbird	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐷 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) )
129	128	ralrimivva	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ) → ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑤 ∈ ( Base ‘ 𝐷 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) )
130	129	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑤 ∈ ( Base ‘ 𝐷 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) )
131		oveq2	⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝑢 ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) 𝑣 ) = ( 𝑢 ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) )
132		oveq2	⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝑢 ( 2^nd ‘ 𝐹 ) 𝑣 ) = ( 𝑢 ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) )
133	131 132	eqeq12d	⊢ ( 𝑣 = ⟨ 𝑧 , 𝑤 ⟩ → ( ( 𝑢 ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) 𝑣 ) = ( 𝑢 ( 2^nd ‘ 𝐹 ) 𝑣 ) ↔ ( 𝑢 ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( 𝑢 ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) )
134	133	ralxp	⊢ ( ∀ 𝑣 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ( 𝑢 ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) 𝑣 ) = ( 𝑢 ( 2^nd ‘ 𝐹 ) 𝑣 ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑤 ∈ ( Base ‘ 𝐷 ) ( 𝑢 ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( 𝑢 ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) )
135		oveq1	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑢 ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) )
136		oveq1	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑢 ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) )
137	135 136	eqeq12d	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑢 ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( 𝑢 ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) )
138	137	2ralbidv	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑤 ∈ ( Base ‘ 𝐷 ) ( 𝑢 ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( 𝑢 ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑤 ∈ ( Base ‘ 𝐷 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) )
139	134 138	bitrid	⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∀ 𝑣 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ( 𝑢 ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) 𝑣 ) = ( 𝑢 ( 2^nd ‘ 𝐹 ) 𝑣 ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑤 ∈ ( Base ‘ 𝐷 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ) )
140	139	ralxp	⊢ ( ∀ 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∀ 𝑣 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ( 𝑢 ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) 𝑣 ) = ( 𝑢 ( 2^nd ‘ 𝐹 ) 𝑣 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑤 ∈ ( Base ‘ 𝐷 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟨ 𝑧 , 𝑤 ⟩ ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) )
141	130 140	sylibr	⊢ ( 𝜑 → ∀ 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∀ 𝑣 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ( 𝑢 ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) 𝑣 ) = ( 𝑢 ( 2^nd ‘ 𝐹 ) 𝑣 ) )
142	26 31	funcfn2	⊢ ( 𝜑 → ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) Fn ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) × ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) )
143	26 35	funcfn2	⊢ ( 𝜑 → ( 2^nd ‘ 𝐹 ) Fn ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) × ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) )
144		eqfnov2	⊢ ( ( ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) Fn ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) × ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ∧ ( 2^nd ‘ 𝐹 ) Fn ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) × ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ) ) → ( ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) = ( 2^nd ‘ 𝐹 ) ↔ ∀ 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∀ 𝑣 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ( 𝑢 ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) 𝑣 ) = ( 𝑢 ( 2^nd ‘ 𝐹 ) 𝑣 ) ) )
145	142 143 144	syl2anc	⊢ ( 𝜑 → ( ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) = ( 2^nd ‘ 𝐹 ) ↔ ∀ 𝑢 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ∀ 𝑣 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ( 𝑢 ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) 𝑣 ) = ( 𝑢 ( 2^nd ‘ 𝐹 ) 𝑣 ) ) )
146	141 145	mpbird	⊢ ( 𝜑 → ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) = ( 2^nd ‘ 𝐹 ) )
147	40 146	opeq12d	⊢ ( 𝜑 → ⟨ ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) , ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟩ = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
148		1st2nd	⊢ ( ( Rel ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ∧ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ) → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) = ⟨ ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) , ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟩ )
149	28 29 148	sylancr	⊢ ( 𝜑 → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) = ⟨ ( 1^st ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) , ( 2^nd ‘ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) ) ⟩ )
150		1st2nd	⊢ ( ( Rel ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ∧ 𝐹 ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐸 ) ) → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
151	28 4 150	sylancr	⊢ ( 𝜑 → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
152	147 149 151	3eqtr4d	⊢ ( 𝜑 → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 ) = 𝐹 )

Metamath Proof Explorer

Theorem uncfcurf

Proof