This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem curf2ndf

Description: As shown in diagval , the currying of the first projection is the diagonal functor. On the other hand, the currying of the second projection is x e. C |-> ( y e. D |-> y ) , which is a constant functor of the identity functor at D . (Contributed by Mario Carneiro, 15-Jan-2017)

Ref Expression
Hypotheses curf2ndf.q ⊢ 𝑄 = ( 𝐷 FuncCat 𝐷 )
curf2ndf.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
curf2ndf.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
Assertion curf2ndf ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) = ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 curf2ndf.q ⊢ 𝑄 = ( 𝐷 FuncCat 𝐷 )
2 curf2ndf.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
3 curf2ndf.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
4 df-ov ⊢ ( 𝑥 ( 1st ‘ ( 𝐶 2ndF 𝐷 ) ) 𝑦 ) = ( ( 1st ‘ ( 𝐶 2ndF 𝐷 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
5 eqid ⊢ ( 𝐶 ×c 𝐷 ) = ( 𝐶 ×c 𝐷 )
6 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
8 5 6 7 xpcbas ⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( Base ‘ ( 𝐶 ×c 𝐷 ) )
9 eqid ⊢ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) = ( Hom ‘ ( 𝐶 ×c 𝐷 ) )
10 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝐶 ∈ Cat )
11 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝐷 ∈ Cat )
12 eqid ⊢ ( 𝐶 2ndF 𝐷 ) = ( 𝐶 2ndF 𝐷 )
13 opelxpi ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
14 13 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
15 5 8 9 10 11 12 14 2ndf1 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1st ‘ ( 𝐶 2ndF 𝐷 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
16 vex ⊢ 𝑥 ∈ V
17 vex ⊢ 𝑦 ∈ V
18 16 17 op2nd ⊢ ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦
19 15 18 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1st ‘ ( 𝐶 2ndF 𝐷 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦 )
20 4 19 eqtrid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑥 ( 1st ‘ ( 𝐶 2ndF 𝐷 ) ) 𝑦 ) = 𝑦 )
21 20 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1st ‘ ( 𝐶 2ndF 𝐷 ) ) 𝑦 ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ 𝑦 ) )
22 mptresid ⊢ ( I ↾ ( Base ‘ 𝐷 ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ 𝑦 )
23 21 22 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1st ‘ ( 𝐶 2ndF 𝐷 ) ) 𝑦 ) ) = ( I ↾ ( Base ‘ 𝐷 ) ) )
24 df-ov ⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( 𝐶 2ndF 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑓 ) = ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( 𝐶 2ndF 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑓 ⟩ )
25 10 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝐶 ∈ Cat )
26 11 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝐷 ∈ Cat )
27 14 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
28 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
29 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝑧 ∈ ( Base ‘ 𝐷 ) )
30 28 29 opelxpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
31 5 8 9 25 26 12 27 30 2ndf2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( 𝐶 2ndF 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) = ( 2nd ↾ ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) ) )
32 31 fveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( 𝐶 2ndF 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑓 ⟩ ) = ( ( 2nd ↾ ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑓 ⟩ ) )
33 24 32 eqtrid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( 𝐶 2ndF 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑓 ) = ( ( 2nd ↾ ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑓 ⟩ ) )
34 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
35 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
36 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
37 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
38 6 34 35 36 37 catidcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
39 38 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
40 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) )
41 39 40 opelxpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑓 ⟩ ∈ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
42 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
43 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
44 5 6 7 34 42 28 43 28 29 9 xpchom2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) = ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) × ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
45 41 44 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑓 ⟩ ∈ ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) )
46 45 fvresd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( 2nd ↾ ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑓 ⟩ ) = ( 2nd ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑓 ⟩ ) )
47 fvex ⊢ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ V
48 vex ⊢ 𝑓 ∈ V
49 47 48 op2nd ⊢ ( 2nd ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑓 ⟩ ) = 𝑓
50 46 49 eqtrdi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( 2nd ↾ ( ⟨ 𝑥 , 𝑦 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , 𝑓 ⟩ ) = 𝑓 )
51 33 50 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( 𝐶 2ndF 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑓 ) = 𝑓 )
52 51 mpteq2dva ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( 𝐶 2ndF 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑓 ) ) = ( 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ 𝑓 ) )
53 mptresid ⊢ ( I ↾ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) = ( 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ 𝑓 )
54 52 53 eqtr4di ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( 𝐶 2ndF 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑓 ) ) = ( I ↾ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
55 54 3impa ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( 𝐶 2ndF 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑓 ) ) = ( I ↾ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
56 55 mpoeq3dva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( 𝐶 2ndF 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑓 ) ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( I ↾ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) )
57 fveq2 ⊢ ( 𝑢 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) = ( ( Hom ‘ 𝐷 ) ‘ ⟨ 𝑦 , 𝑧 ⟩ ) )
58 df-ov ⊢ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) = ( ( Hom ‘ 𝐷 ) ‘ ⟨ 𝑦 , 𝑧 ⟩ )
59 57 58 eqtr4di ⊢ ( 𝑢 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) = ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) )
60 59 reseq2d ⊢ ( 𝑢 = ⟨ 𝑦 , 𝑧 ⟩ → ( I ↾ ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) ) = ( I ↾ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
61 60 mpompt ⊢ ( 𝑢 ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ↦ ( I ↾ ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) ) ) = ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( I ↾ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
62 56 61 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( 𝐶 2ndF 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑓 ) ) ) = ( 𝑢 ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ↦ ( I ↾ ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) ) ) )
63 23 62 opeq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1st ‘ ( 𝐶 2ndF 𝐷 ) ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( 𝐶 2ndF 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑓 ) ) ) ⟩ = ⟨ ( I ↾ ( Base ‘ 𝐷 ) ) , ( 𝑢 ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ↦ ( I ↾ ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) ) ) ⟩ )
64 eqid ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) = ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) )
65 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐷 ∈ Cat )
66 5 2 3 12 2ndfcl ⊢ ( 𝜑 → ( 𝐶 2ndF 𝐷 ) ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐷 ) )
67 66 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝐶 2ndF 𝐷 ) ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐷 ) )
68 eqid ⊢ ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) ‘ 𝑥 ) = ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) ‘ 𝑥 )
69 64 6 36 65 67 7 37 68 42 35 curf1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) ‘ 𝑥 ) = ⟨ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 ( 1st ‘ ( 𝐶 2ndF 𝐷 ) ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝐷 ) , 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( 2nd ‘ ( 𝐶 2ndF 𝐷 ) ) ⟨ 𝑥 , 𝑧 ⟩ ) 𝑓 ) ) ) ⟩ )
70 eqid ⊢ ( idfunc ‘ 𝐷 ) = ( idfunc ‘ 𝐷 )
71 70 7 65 42 idfuval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( idfunc ‘ 𝐷 ) = ⟨ ( I ↾ ( Base ‘ 𝐷 ) ) , ( 𝑢 ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ↦ ( I ↾ ( ( Hom ‘ 𝐷 ) ‘ 𝑢 ) ) ) ⟩ )
72 63 69 71 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) ‘ 𝑥 ) = ( idfunc ‘ 𝐷 ) )
73 eqid ⊢ ( 𝑄 Δfunc 𝐶 ) = ( 𝑄 Δfunc 𝐶 )
74 1 3 3 fuccat ⊢ ( 𝜑 → 𝑄 ∈ Cat )
75 74 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑄 ∈ Cat )
76 1 fucbas ⊢ ( 𝐷 Func 𝐷 ) = ( Base ‘ 𝑄 )
77 70 idfucl ⊢ ( 𝐷 ∈ Cat → ( idfunc ‘ 𝐷 ) ∈ ( 𝐷 Func 𝐷 ) )
78 3 77 syl ⊢ ( 𝜑 → ( idfunc ‘ 𝐷 ) ∈ ( 𝐷 Func 𝐷 ) )
79 78 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( idfunc ‘ 𝐷 ) ∈ ( 𝐷 Func 𝐷 ) )
80 eqid ⊢ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) = ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) )
81 73 75 36 76 79 80 6 37 diag11 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) ‘ 𝑥 ) = ( idfunc ‘ 𝐷 ) )
82 72 81 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) ‘ 𝑥 ) = ( ( 1st ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) ‘ 𝑥 ) )
83 82 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) ‘ 𝑥 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1st ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) ‘ 𝑥 ) ) )
84 relfunc ⊢ Rel ( 𝐶 Func 𝑄 )
85 64 1 2 3 66 curfcl ⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ∈ ( 𝐶 Func 𝑄 ) )
86 1st2ndbr ⊢ ( ( Rel ( 𝐶 Func 𝑄 ) ∧ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ∈ ( 𝐶 Func 𝑄 ) ) → ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) ( 𝐶 Func 𝑄 ) ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) )
87 84 85 86 sylancr ⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) ( 𝐶 Func 𝑄 ) ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) )
88 6 76 87 funcf1 ⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) : ( Base ‘ 𝐶 ) ⟶ ( 𝐷 Func 𝐷 ) )
89 88 feqmptd ⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) ‘ 𝑥 ) ) )
90 73 74 2 76 78 80 diag1cl ⊢ ( 𝜑 → ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ∈ ( 𝐶 Func 𝑄 ) )
91 1st2ndbr ⊢ ( ( Rel ( 𝐶 Func 𝑄 ) ∧ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ∈ ( 𝐶 Func 𝑄 ) ) → ( 1st ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) ( 𝐶 Func 𝑄 ) ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) )
92 84 90 91 sylancr ⊢ ( 𝜑 → ( 1st ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) ( 𝐶 Func 𝑄 ) ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) )
93 6 76 92 funcf1 ⊢ ( 𝜑 → ( 1st ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) : ( Base ‘ 𝐶 ) ⟶ ( 𝐷 Func 𝐷 ) )
94 93 feqmptd ⊢ ( 𝜑 → ( 1st ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1st ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) ‘ 𝑥 ) ) )
95 83 89 94 3eqtr4d ⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) = ( 1st ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) )
96 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐷 ∈ Cat )
97 70 7 96 idfu1st ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 1st ‘ ( idfunc ‘ 𝐷 ) ) = ( I ↾ ( Base ‘ 𝐷 ) ) )
98 97 coeq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( Id ‘ 𝐷 ) ∘ ( 1st ‘ ( idfunc ‘ 𝐷 ) ) ) = ( ( Id ‘ 𝐷 ) ∘ ( I ↾ ( Base ‘ 𝐷 ) ) ) )
99 eqid ⊢ ( Id ‘ 𝑄 ) = ( Id ‘ 𝑄 )
100 eqid ⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
101 78 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( idfunc ‘ 𝐷 ) ∈ ( 𝐷 Func 𝐷 ) )
102 1 99 100 101 fucid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( Id ‘ 𝑄 ) ‘ ( idfunc ‘ 𝐷 ) ) = ( ( Id ‘ 𝐷 ) ∘ ( 1st ‘ ( idfunc ‘ 𝐷 ) ) ) )
103 7 100 cidfn ⊢ ( 𝐷 ∈ Cat → ( Id ‘ 𝐷 ) Fn ( Base ‘ 𝐷 ) )
104 96 103 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( Id ‘ 𝐷 ) Fn ( Base ‘ 𝐷 ) )
105 dffn2 ⊢ ( ( Id ‘ 𝐷 ) Fn ( Base ‘ 𝐷 ) ↔ ( Id ‘ 𝐷 ) : ( Base ‘ 𝐷 ) ⟶ V )
106 104 105 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( Id ‘ 𝐷 ) : ( Base ‘ 𝐷 ) ⟶ V )
107 106 feqmptd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( Id ‘ 𝐷 ) = ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) )
108 fcoi1 ⊢ ( ( Id ‘ 𝐷 ) : ( Base ‘ 𝐷 ) ⟶ V → ( ( Id ‘ 𝐷 ) ∘ ( I ↾ ( Base ‘ 𝐷 ) ) ) = ( Id ‘ 𝐷 ) )
109 106 108 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( Id ‘ 𝐷 ) ∘ ( I ↾ ( Base ‘ 𝐷 ) ) ) = ( Id ‘ 𝐷 ) )
110 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐶 ∈ Cat )
111 110 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → 𝐶 ∈ Cat )
112 96 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → 𝐷 ∈ Cat )
113 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
114 opelxpi ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
115 113 114 sylan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
116 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
117 opelxpi ⊢ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
118 116 117 sylan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
119 5 8 9 111 112 12 115 118 2ndf2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ ( 𝐶 2ndF 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) = ( 2nd ↾ ( ⟨ 𝑥 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ) )
120 119 oveqd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑓 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ ( 𝐶 2ndF 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) = ( 𝑓 ( 2nd ↾ ( ⟨ 𝑥 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) )
121 df-ov ⊢ ( 𝑓 ( 2nd ↾ ( ⟨ 𝑥 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) = ( ( 2nd ↾ ( ⟨ 𝑥 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ) ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ⟩ )
122 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
123 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → 𝑧 ∈ ( Base ‘ 𝐷 ) )
124 7 42 100 112 123 catidcl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑧 ) )
125 122 124 opelxpd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ⟩ ∈ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( 𝑧 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
126 113 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
127 116 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
128 5 6 7 34 42 126 123 127 123 9 xpchom2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( ⟨ 𝑥 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) = ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( 𝑧 ( Hom ‘ 𝐷 ) 𝑧 ) ) )
129 125 128 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ⟩ ∈ ( ⟨ 𝑥 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) )
130 129 fvresd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( ( 2nd ↾ ( ⟨ 𝑥 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ) ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ⟩ ) = ( 2nd ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ⟩ ) )
131 121 130 eqtrid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑓 ( 2nd ↾ ( ⟨ 𝑥 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) = ( 2nd ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ⟩ ) )
132 fvex ⊢ ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ∈ V
133 48 132 op2nd ⊢ ( 2nd ‘ ⟨ 𝑓 , ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ⟩ ) = ( ( Id ‘ 𝐷 ) ‘ 𝑧 )
134 131 133 eqtrdi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑓 ( 2nd ↾ ( ⟨ 𝑥 , 𝑧 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) = ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) )
135 120 134 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) → ( 𝑓 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ ( 𝐶 2ndF 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) = ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) )
136 135 mpteq2dva ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑓 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ ( 𝐶 2ndF 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) )
137 107 109 136 3eqtr4rd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑓 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ ( 𝐶 2ndF 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) = ( ( Id ‘ 𝐷 ) ∘ ( I ↾ ( Base ‘ 𝐷 ) ) ) )
138 98 102 137 3eqtr4rd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑓 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ ( 𝐶 2ndF 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) = ( ( Id ‘ 𝑄 ) ‘ ( idfunc ‘ 𝐷 ) ) )
139 66 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 𝐶 2ndF 𝐷 ) ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐷 ) )
140 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
141 eqid ⊢ ( ( 𝑥 ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) 𝑦 ) ‘ 𝑓 ) = ( ( 𝑥 ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) 𝑦 ) ‘ 𝑓 )
142 64 6 110 96 139 7 34 100 113 116 140 141 curf2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) 𝑦 ) ‘ 𝑓 ) = ( 𝑧 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑓 ( ⟨ 𝑥 , 𝑧 ⟩ ( 2nd ‘ ( 𝐶 2ndF 𝐷 ) ) ⟨ 𝑦 , 𝑧 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) )
143 74 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑄 ∈ Cat )
144 73 143 110 76 101 80 6 113 34 99 116 140 diag12 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) 𝑦 ) ‘ 𝑓 ) = ( ( Id ‘ 𝑄 ) ‘ ( idfunc ‘ 𝐷 ) ) )
145 138 142 144 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) 𝑦 ) ‘ 𝑓 ) = ( ( 𝑥 ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) 𝑦 ) ‘ 𝑓 ) )
146 145 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( 𝑥 ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) 𝑦 ) ‘ 𝑓 ) ) = ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( 𝑥 ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) 𝑦 ) ‘ 𝑓 ) ) )
147 eqid ⊢ ( 𝐷 Nat 𝐷 ) = ( 𝐷 Nat 𝐷 )
148 1 147 fuchom ⊢ ( 𝐷 Nat 𝐷 ) = ( Hom ‘ 𝑄 )
149 87 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) ( 𝐶 Func 𝑄 ) ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) )
150 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
151 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
152 6 34 148 149 150 151 funcf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐷 ) ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) ‘ 𝑦 ) ) )
153 152 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) 𝑦 ) = ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( 𝑥 ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) 𝑦 ) ‘ 𝑓 ) ) )
154 92 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1st ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) ( 𝐶 Func 𝑄 ) ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) )
155 6 34 148 154 150 151 funcf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1st ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) ‘ 𝑥 ) ( 𝐷 Nat 𝐷 ) ( ( 1st ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) ‘ 𝑦 ) ) )
156 155 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) 𝑦 ) = ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( 𝑥 ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) 𝑦 ) ‘ 𝑓 ) ) )
157 146 153 156 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) 𝑦 ) = ( 𝑥 ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) 𝑦 ) )
158 157 3impb ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) 𝑦 ) = ( 𝑥 ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) 𝑦 ) )
159 158 mpoeq3dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) 𝑦 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) 𝑦 ) ) )
160 6 87 funcfn2 ⊢ ( 𝜑 → ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
161 fnov ⊢ ( ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) 𝑦 ) ) )
162 160 161 sylib ⊢ ( 𝜑 → ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) 𝑦 ) ) )
163 6 92 funcfn2 ⊢ ( 𝜑 → ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
164 fnov ⊢ ( ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) 𝑦 ) ) )
165 163 164 sylib ⊢ ( 𝜑 → ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) 𝑦 ) ) )
166 159 162 165 3eqtr4d ⊢ ( 𝜑 → ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) = ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) )
167 95 166 opeq12d ⊢ ( 𝜑 → ⟨ ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) , ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) ⟩ = ⟨ ( 1st ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) , ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) ⟩ )
168 1st2nd ⊢ ( ( Rel ( 𝐶 Func 𝑄 ) ∧ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ∈ ( 𝐶 Func 𝑄 ) ) → ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) = ⟨ ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) , ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) ⟩ )
169 84 85 168 sylancr ⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) = ⟨ ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) , ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) ) ⟩ )
170 1st2nd ⊢ ( ( Rel ( 𝐶 Func 𝑄 ) ∧ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ∈ ( 𝐶 Func 𝑄 ) ) → ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) = ⟨ ( 1st ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) , ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) ⟩ )
171 84 90 170 sylancr ⊢ ( 𝜑 → ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) = ⟨ ( 1st ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) , ( 2nd ‘ ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) ) ⟩ )
172 167 169 171 3eqtr4d ⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ curryF ( 𝐶 2ndF 𝐷 ) ) = ( ( 1st ‘ ( 𝑄 Δfunc 𝐶 ) ) ‘ ( idfunc ‘ 𝐷 ) ) )