Metamath Proof Explorer

Theorem fuccofval

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

Ref Expression
Hypotheses fucval.q ⊢ Q = C FuncCat D
fucval.b ⊢ B = C Func D
fucval.n ⊢ N = C Nat D
fucval.a ⊢ A = Base C
fucval.o ⊢ · ˙ = comp ⁡ D
fucval.c ⊢ φ → C ∈ Cat
fucval.d ⊢ φ → D ∈ Cat
fuccofval.x ⊢ ∙ ˙ = comp ⁡ Q
Assertion fuccofval ⊢ φ → ∙ ˙ = v ∈ B × B , h ∈ B ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g N h , a ∈ f N g ⟼ x ∈ A ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x · ˙ 1 st ⁡ h ⁡ x a ⁡ x

Proof

Step Hyp Ref Expression
1 fucval.q ⊢ Q = C FuncCat D
2 fucval.b ⊢ B = C Func D
3 fucval.n ⊢ N = C Nat D
4 fucval.a ⊢ A = Base C
5 fucval.o ⊢ · ˙ = comp ⁡ D
6 fucval.c ⊢ φ → C ∈ Cat
7 fucval.d ⊢ φ → D ∈ Cat
8 fuccofval.x ⊢ ∙ ˙ = comp ⁡ Q
9 eqidd ⊢ φ → v ∈ B × B , h ∈ B ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g N h , a ∈ f N g ⟼ x ∈ A ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x · ˙ 1 st ⁡ h ⁡ x a ⁡ x = v ∈ B × B , h ∈ B ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g N h , a ∈ f N g ⟼ x ∈ A ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x · ˙ 1 st ⁡ h ⁡ x a ⁡ x
10 1 2 3 4 5 6 7 9 fucval ⊢ φ → Q = Base ndx B Hom ⁡ ndx N comp ⁡ ndx v ∈ B × B , h ∈ B ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g N h , a ∈ f N g ⟼ x ∈ A ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x · ˙ 1 st ⁡ h ⁡ x a ⁡ x
11 10 fveq2d ⊢ φ → comp ⁡ Q = comp ⁡ Base ndx B Hom ⁡ ndx N comp ⁡ ndx v ∈ B × B , h ∈ B ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g N h , a ∈ f N g ⟼ x ∈ A ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x · ˙ 1 st ⁡ h ⁡ x a ⁡ x
12 2 ovexi ⊢ B ∈ V
13 12 12 xpex ⊢ B × B ∈ V
14 13 12 mpoex ⊢ v ∈ B × B , h ∈ B ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g N h , a ∈ f N g ⟼ x ∈ A ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x · ˙ 1 st ⁡ h ⁡ x a ⁡ x ∈ V
15 catstr ⊢ Base ndx B Hom ⁡ ndx N comp ⁡ ndx v ∈ B × B , h ∈ B ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g N h , a ∈ f N g ⟼ x ∈ A ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x · ˙ 1 st ⁡ h ⁡ x a ⁡ x Struct 1 15
16 ccoid ⊢ comp = Slot comp ⁡ ndx
17 snsstp3 ⊢ comp ⁡ ndx v ∈ B × B , h ∈ B ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g N h , a ∈ f N g ⟼ x ∈ A ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x · ˙ 1 st ⁡ h ⁡ x a ⁡ x ⊆ Base ndx B Hom ⁡ ndx N comp ⁡ ndx v ∈ B × B , h ∈ B ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g N h , a ∈ f N g ⟼ x ∈ A ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x · ˙ 1 st ⁡ h ⁡ x a ⁡ x
18 15 16 17 strfv ⊢ v ∈ B × B , h ∈ B ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g N h , a ∈ f N g ⟼ x ∈ A ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x · ˙ 1 st ⁡ h ⁡ x a ⁡ x ∈ V → v ∈ B × B , h ∈ B ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g N h , a ∈ f N g ⟼ x ∈ A ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x · ˙ 1 st ⁡ h ⁡ x a ⁡ x = comp ⁡ Base ndx B Hom ⁡ ndx N comp ⁡ ndx v ∈ B × B , h ∈ B ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g N h , a ∈ f N g ⟼ x ∈ A ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x · ˙ 1 st ⁡ h ⁡ x a ⁡ x
19 14 18 ax-mp ⊢ v ∈ B × B , h ∈ B ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g N h , a ∈ f N g ⟼ x ∈ A ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x · ˙ 1 st ⁡ h ⁡ x a ⁡ x = comp ⁡ Base ndx B Hom ⁡ ndx N comp ⁡ ndx v ∈ B × B , h ∈ B ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g N h , a ∈ f N g ⟼ x ∈ A ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x · ˙ 1 st ⁡ h ⁡ x a ⁡ x
20 11 8 19 3eqtr4g ⊢ φ → ∙ ˙ = v ∈ B × B , h ∈ B ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g N h , a ∈ f N g ⟼ x ∈ A ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x · ˙ 1 st ⁡ h ⁡ x a ⁡ x