fuccofval

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 )
	fuccofval.x	⊢ ∙ = ( comp ‘ 𝑄 )
Assertion	fuccofval	⊢ ( 𝜑 → ∙ = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , ℎ ∈ 𝐵 ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) )

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		fuccofval.x	⊢ ∙ = ( comp ‘ 𝑄 )
9		eqidd	⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , ℎ ∈ 𝐵 ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , ℎ ∈ 𝐵 ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
10	1 2 3 4 5 6 7 9	fucval	⊢ ( 𝜑 → 𝑄 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝑁 ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , ℎ ∈ 𝐵 ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } )
11	10	fveq2d	⊢ ( 𝜑 → ( comp ‘ 𝑄 ) = ( comp ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝑁 ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , ℎ ∈ 𝐵 ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } ) )
12	2	ovexi	⊢ 𝐵 ∈ V
13	12 12	xpex	⊢ ( 𝐵 × 𝐵 ) ∈ V
14	13 12	mpoex	⊢ ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , ℎ ∈ 𝐵 ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ∈ V
15		catstr	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝑁 ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , ℎ ∈ 𝐵 ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } Struct ⟨ 1 , ; 1 5 ⟩
16		ccoid	⊢ comp = Slot ( comp ‘ ndx )
17		snsstp3	⊢ { ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , ℎ ∈ 𝐵 ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝑁 ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , ℎ ∈ 𝐵 ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ }
18	15 16 17	strfv	⊢ ( ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , ℎ ∈ 𝐵 ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ∈ V → ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , ℎ ∈ 𝐵 ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ( comp ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝑁 ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , ℎ ∈ 𝐵 ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } ) )
19	14 18	ax-mp	⊢ ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , ℎ ∈ 𝐵 ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ( comp ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝑁 ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , ℎ ∈ 𝐵 ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } )
20	11 8 19	3eqtr4g	⊢ ( 𝜑 → ∙ = ( 𝑣 ∈ ( 𝐵 × 𝐵 ) , ℎ ∈ 𝐵 ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 𝑁 ℎ ) , 𝑎 ∈ ( 𝑓 𝑁 𝑔 ) ↦ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ · ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) )

Metamath Proof Explorer

Theorem fuccofval

Proof