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 

dfov 
⊢ ( 𝑥 ( 1^{st} ‘ 𝐹 ) 𝑦 ) = ( ( 1^{st} ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) 
61 
59 60

syl6eq 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 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 

dfov 
⊢ ( 𝑥 ( 1^{st} ‘ 𝐹 ) 𝑤 ) = ( ( 1^{st} ‘ 𝐹 ) ‘ ⟨ 𝑥 , 𝑤 ⟩ ) 
64 
62 63

syl6eq 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 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 

dfov 
⊢ ( 𝑧 ( 1^{st} ‘ 𝐹 ) 𝑤 ) = ( ( 1^{st} ‘ 𝐹 ) ‘ ⟨ 𝑧 , 𝑤 ⟩ ) 
69 
67 68

syl6eq 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 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 

dfov 
⊢ ( 𝑓 ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^{nd} ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ) = ( ( ⟨ 𝑥 , 𝑤 ⟩ ( 2^{nd} ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ⟩ ) 
75 
73 74

syl6eq 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 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 

dfov 
⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^{nd} ‘ 𝐹 ) ⟨ 𝑥 , 𝑤 ⟩ ) 𝑔 ) = ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^{nd} ‘ 𝐹 ) ⟨ 𝑥 , 𝑤 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑔 ⟩ ) 
79 
77 78

syl6eq 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 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 

dfov 
⊢ ( ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^{nd} ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ( ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ( ⟨ 𝑦 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ) = ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2^{nd} ‘ 𝐹 ) ⟨ 𝑧 , 𝑤 ⟩ ) ‘ ⟨ ( 𝑓 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) , ( ( ( Id ‘ 𝐷 ) ‘ 𝑤 ) ( ⟨ 𝑦 , 𝑤 ⟩ ( comp ‘ 𝐷 ) 𝑤 ) 𝑔 ) ⟩ ) 
107 
105 106

syl6eqr 
⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 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

syl5bb 
⊢ ( 𝑢 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∀ 𝑣 ∈ ( ( 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} 𝐺 ) = 𝐹 ) 