fucval

Description: Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	fucval.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	fucval.b	⊢ 𝐵 = ( 𝐶 Func 𝐷 )
	fucval.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	fucval.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	fucval.o	⊢ · = ( comp ‘ 𝐷 )
	fucval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	fucval.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	fucval.x	⊢ ( 𝜑 → ∙ = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , ℎ ∈ 𝐵 ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
Assertion	fucval	⊢ ( 𝜑 → 𝑄 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝑁 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		fucval.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		fucval.b	⊢ 𝐵 = ( 𝐶 Func 𝐷 )
3		fucval.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
4		fucval.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
5		fucval.o	⊢ · = ( comp ‘ 𝐷 )
6		fucval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
7		fucval.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
8		fucval.x	⊢ ( 𝜑 → ∙ = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , ℎ ∈ 𝐵 ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
9		df-fuc	⊢ FuncCat = ( 𝑡 ∈ Cat , 𝑢 ∈ Cat ↦ { ⟨ ( Base ‘ ndx ) , ( 𝑡 Func 𝑢 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑡 Nat 𝑢 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) , ℎ ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } )
10	9	a1i	⊢ ( 𝜑 → FuncCat = ( 𝑡 ∈ Cat , 𝑢 ∈ Cat ↦ { ⟨ ( Base ‘ ndx ) , ( 𝑡 Func 𝑢 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑡 Nat 𝑢 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) , ℎ ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } ) )
11		simprl	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → 𝑡 = 𝐶 )
12		simprr	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → 𝑢 = 𝐷 )
13	11 12	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ( 𝑡 Func 𝑢 ) = ( 𝐶 Func 𝐷 ) )
14	13 2	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ( 𝑡 Func 𝑢 ) = 𝐵 )
15	14	opeq2d	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ⟨ ( Base ‘ ndx ) , ( 𝑡 Func 𝑢 ) ⟩ = ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ )
16	11 12	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ( 𝑡 Nat 𝑢 ) = ( 𝐶 Nat 𝐷 ) )
17	16 3	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ( 𝑡 Nat 𝑢 ) = 𝑁 )
18	17	opeq2d	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ⟨ ( Hom ‘ ndx ) , ( 𝑡 Nat 𝑢 ) ⟩ = ⟨ ( Hom ‘ ndx ) , 𝑁 ⟩ )
19	14	sqxpeqd	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) = ( 𝐵 × 𝐵 ) )
20	17	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) = ( 𝑔 𝑁 ℎ ) )
21	17	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) = ( 𝑓 𝑁 𝑔 ) )
22	11	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ( Base ‘ 𝑡 ) = ( Base ‘ 𝐶 ) )
23	22 4	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ( Base ‘ 𝑡 ) = 𝐴 )
24	12	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ( comp ‘ 𝑢 ) = ( comp ‘ 𝐷 ) )
25	24 5	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ( comp ‘ 𝑢 ) = · )
26	25	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) = ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) )
27	26	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) = ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) )
28	23 27	mpteq12dv	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
29	20 21 28	mpoeq123dv	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) = ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
30	29	csbeq2dv	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) = ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
31	30	csbeq2dv	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) = ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
32	19 14 31	mpoeq123dv	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ( 𝑣 ∈ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) , ℎ ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , ℎ ∈ 𝐵 ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
33	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ∙ = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , ℎ ∈ 𝐵 ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
34	32 33	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ( 𝑣 ∈ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) , ℎ ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ∙ )
35	34	opeq2d	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) , ℎ ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ = ⟨ ( comp ‘ ndx ) , ∙ ⟩ )
36	15 18 35	tpeq123d	⊢ ( ( 𝜑 ∧ ( 𝑡 = 𝐶 ∧ 𝑢 = 𝐷 ) ) → { ⟨ ( Base ‘ ndx ) , ( 𝑡 Func 𝑢 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑡 Nat 𝑢 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) , ℎ ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝑁 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } )
37		tpex	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝑁 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ∈ V
38	37	a1i	⊢ ( 𝜑 → { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝑁 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ∈ V )
39	10 36 6 7 38	ovmpod	⊢ ( 𝜑 → ( 𝐶 FuncCat 𝐷 ) = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝑁 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } )
40	1 39	syl5eq	⊢ ( 𝜑 → 𝑄 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝑁 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } )

Metamath Proof Explorer

Theorem fucval

Proof