Theorem uncfval

Description: Value of the uncurry functor, which is the reverse of the curry functor, taking G : C --> ( D --> E ) to uncurryF ( G ) : C X. D --> E . (Contributed by Mario Carneiro, 13-Jan-2017)

	Ref	Expression
Hypotheses	uncfval.g	⊢ 𝐹 = ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 )
	uncfval.c	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	uncfval.d	⊢ ( 𝜑 → 𝐸 ∈ Cat )
	uncfval.f	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) )
Assertion	uncfval	⊢ ( 𝜑 → 𝐹 = ( ( 𝐷 evalF 𝐸 ) ∘func ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ⟨,⟩F ( 𝐶 2ndF 𝐷 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		uncfval.g	⊢ 𝐹 = ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 )
2		uncfval.c	⊢ ( 𝜑 → 𝐷 ∈ Cat )
3		uncfval.d	⊢ ( 𝜑 → 𝐸 ∈ Cat )
4		uncfval.f	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) )
5		df-uncf	⊢ uncurryF = ( 𝑐 ∈ V , 𝑓 ∈ V ↦ ( ( ( 𝑐 ‘ 1 ) evalF ( 𝑐 ‘ 2 ) ) ∘func ( ( 𝑓 ∘func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) ) ⟨,⟩F ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) ) ) ) )
6	5	a1i	⊢ ( 𝜑 → uncurryF = ( 𝑐 ∈ V , 𝑓 ∈ V ↦ ( ( ( 𝑐 ‘ 1 ) evalF ( 𝑐 ‘ 2 ) ) ∘func ( ( 𝑓 ∘func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) ) ⟨,⟩F ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) ) ) ) ) )
7		simprl	⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ )
8	7	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( 𝑐 ‘ 1 ) = ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 1 ) )
9		s3fv1	⊢ ( 𝐷 ∈ Cat → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 1 ) = 𝐷 )
10	2 9	syl	⊢ ( 𝜑 → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 1 ) = 𝐷 )
11	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 1 ) = 𝐷 )
12	8 11	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( 𝑐 ‘ 1 ) = 𝐷 )
13	7	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( 𝑐 ‘ 2 ) = ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 2 ) )
14		s3fv2	⊢ ( 𝐸 ∈ Cat → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 2 ) = 𝐸 )
15	3 14	syl	⊢ ( 𝜑 → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 2 ) = 𝐸 )
16	15	adantr	⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 2 ) = 𝐸 )
17	13 16	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( 𝑐 ‘ 2 ) = 𝐸 )
18	12 17	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( ( 𝑐 ‘ 1 ) evalF ( 𝑐 ‘ 2 ) ) = ( 𝐷 evalF 𝐸 ) )
19		simprr	⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → 𝑓 = 𝐺 )
20	7	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( 𝑐 ‘ 0 ) = ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 0 ) )
21		funcrcl	⊢ ( 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) → ( 𝐶 ∈ Cat ∧ ( 𝐷 FuncCat 𝐸 ) ∈ Cat ) )
22	4 21	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( 𝐷 FuncCat 𝐸 ) ∈ Cat ) )
23	22	simpld	⊢ ( 𝜑 → 𝐶 ∈ Cat )
24		s3fv0	⊢ ( 𝐶 ∈ Cat → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 0 ) = 𝐶 )
25	23 24	syl	⊢ ( 𝜑 → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 0 ) = 𝐶 )
26	25	adantr	⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ‘ 0 ) = 𝐶 )
27	20 26	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( 𝑐 ‘ 0 ) = 𝐶 )
28	27 12	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) = ( 𝐶 1stF 𝐷 ) )
29	19 28	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( 𝑓 ∘func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) ) = ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) )
30	27 12	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) ) = ( 𝐶 2ndF 𝐷 ) )
31	29 30	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( ( 𝑓 ∘func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) ) ⟨,⟩F ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) ) ) = ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ⟨,⟩F ( 𝐶 2ndF 𝐷 ) ) )
32	18 31	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑐 = ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∧ 𝑓 = 𝐺 ) ) → ( ( ( 𝑐 ‘ 1 ) evalF ( 𝑐 ‘ 2 ) ) ∘func ( ( 𝑓 ∘func ( ( 𝑐 ‘ 0 ) 1stF ( 𝑐 ‘ 1 ) ) ) ⟨,⟩F ( ( 𝑐 ‘ 0 ) 2ndF ( 𝑐 ‘ 1 ) ) ) ) = ( ( 𝐷 evalF 𝐸 ) ∘func ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ⟨,⟩F ( 𝐶 2ndF 𝐷 ) ) ) )
33		s3cli	⊢ ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∈ Word V
34		elex	⊢ ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∈ Word V → ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∈ V )
35	33 34	mp1i	⊢ ( 𝜑 → ⟨“ 𝐶 𝐷 𝐸 ”⟩ ∈ V )
36	4	elexd	⊢ ( 𝜑 → 𝐺 ∈ V )
37		ovexd	⊢ ( 𝜑 → ( ( 𝐷 evalF 𝐸 ) ∘func ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ⟨,⟩F ( 𝐶 2ndF 𝐷 ) ) ) ∈ V )
38	6 32 35 36 37	ovmpod	⊢ ( 𝜑 → ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 ) = ( ( 𝐷 evalF 𝐸 ) ∘func ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ⟨,⟩F ( 𝐶 2ndF 𝐷 ) ) ) )
39	1 38	eqtrid	⊢ ( 𝜑 → 𝐹 = ( ( 𝐷 evalF 𝐸 ) ∘func ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ⟨,⟩F ( 𝐶 2ndF 𝐷 ) ) ) )