Metamath Proof Explorer

Theorem yonedalem4a

Description: Lemma for yoneda . (Contributed by Mario Carneiro, 29-Jan-2017)

Ref Expression
Hypotheses yoneda.y ⊢ Y = Yon ⁡ C
yoneda.b ⊢ B = Base C
yoneda.1 ⊢ 1 ˙ = Id ⁡ C
yoneda.o ⊢ O = oppCat ⁡ C
yoneda.s ⊢ S = SetCat ⁡ U
yoneda.t ⊢ T = SetCat ⁡ V
yoneda.q ⊢ Q = O FuncCat S
yoneda.h ⊢ H = Hom F ⁡ Q
yoneda.r ⊢ R = Q × c O FuncCat T
yoneda.e ⊢ E = O eval F S
yoneda.z ⊢ Z = H ∘ func 1 st ⁡ Y tpos 2 nd ⁡ Y ∘ func Q 2 nd F O ⟨,⟩ F Q 1 st F O
yoneda.c ⊢ φ → C ∈ Cat
yoneda.w ⊢ φ → V ∈ W
yoneda.u ⊢ φ → ran ⁡ Hom 𝑓 ⁡ C ⊆ U
yoneda.v ⊢ φ → ran ⁡ Hom 𝑓 ⁡ Q ∪ U ⊆ V
yonedalem21.f ⊢ φ → F ∈ O Func S
yonedalem21.x ⊢ φ → X ∈ B
yonedalem4.n ⊢ N = f ∈ O Func S , x ∈ B ⟼ u ∈ 1 st ⁡ f ⁡ x ⟼ y ∈ B ⟼ g ∈ y Hom ⁡ C x ⟼ x 2 nd ⁡ f y ⁡ g ⁡ u
yonedalem4.p ⊢ φ → A ∈ 1 st ⁡ F ⁡ X
Assertion yonedalem4a ⊢ φ → F N X ⁡ A = y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A

Proof

Step Hyp Ref Expression
1 yoneda.y ⊢ Y = Yon ⁡ C
2 yoneda.b ⊢ B = Base C
3 yoneda.1 ⊢ 1 ˙ = Id ⁡ C
4 yoneda.o ⊢ O = oppCat ⁡ C
5 yoneda.s ⊢ S = SetCat ⁡ U
6 yoneda.t ⊢ T = SetCat ⁡ V
7 yoneda.q ⊢ Q = O FuncCat S
8 yoneda.h ⊢ H = Hom F ⁡ Q
9 yoneda.r ⊢ R = Q × c O FuncCat T
10 yoneda.e ⊢ E = O eval F S
11 yoneda.z ⊢ Z = H ∘ func 1 st ⁡ Y tpos 2 nd ⁡ Y ∘ func Q 2 nd F O ⟨,⟩ F Q 1 st F O
12 yoneda.c ⊢ φ → C ∈ Cat
13 yoneda.w ⊢ φ → V ∈ W
14 yoneda.u ⊢ φ → ran ⁡ Hom 𝑓 ⁡ C ⊆ U
15 yoneda.v ⊢ φ → ran ⁡ Hom 𝑓 ⁡ Q ∪ U ⊆ V
16 yonedalem21.f ⊢ φ → F ∈ O Func S
17 yonedalem21.x ⊢ φ → X ∈ B
18 yonedalem4.n ⊢ N = f ∈ O Func S , x ∈ B ⟼ u ∈ 1 st ⁡ f ⁡ x ⟼ y ∈ B ⟼ g ∈ y Hom ⁡ C x ⟼ x 2 nd ⁡ f y ⁡ g ⁡ u
19 yonedalem4.p ⊢ φ → A ∈ 1 st ⁡ F ⁡ X
20 18 a1i ⊢ φ → N = f ∈ O Func S , x ∈ B ⟼ u ∈ 1 st ⁡ f ⁡ x ⟼ y ∈ B ⟼ g ∈ y Hom ⁡ C x ⟼ x 2 nd ⁡ f y ⁡ g ⁡ u
21 simprl ⊢ φ ∧ f = F ∧ x = X → f = F
22 21 fveq2d ⊢ φ ∧ f = F ∧ x = X → 1 st ⁡ f = 1 st ⁡ F
23 simprr ⊢ φ ∧ f = F ∧ x = X → x = X
24 22 23 fveq12d ⊢ φ ∧ f = F ∧ x = X → 1 st ⁡ f ⁡ x = 1 st ⁡ F ⁡ X
25 simplrr ⊢ φ ∧ f = F ∧ x = X ∧ y ∈ B → x = X
26 25 oveq2d ⊢ φ ∧ f = F ∧ x = X ∧ y ∈ B → y Hom ⁡ C x = y Hom ⁡ C X
27 simplrl ⊢ φ ∧ f = F ∧ x = X ∧ y ∈ B → f = F
28 27 fveq2d ⊢ φ ∧ f = F ∧ x = X ∧ y ∈ B → 2 nd ⁡ f = 2 nd ⁡ F
29 eqidd ⊢ φ ∧ f = F ∧ x = X ∧ y ∈ B → y = y
30 28 25 29 oveq123d ⊢ φ ∧ f = F ∧ x = X ∧ y ∈ B → x 2 nd ⁡ f y = X 2 nd ⁡ F y
31 30 fveq1d ⊢ φ ∧ f = F ∧ x = X ∧ y ∈ B → x 2 nd ⁡ f y ⁡ g = X 2 nd ⁡ F y ⁡ g
32 31 fveq1d ⊢ φ ∧ f = F ∧ x = X ∧ y ∈ B → x 2 nd ⁡ f y ⁡ g ⁡ u = X 2 nd ⁡ F y ⁡ g ⁡ u
33 26 32 mpteq12dv ⊢ φ ∧ f = F ∧ x = X ∧ y ∈ B → g ∈ y Hom ⁡ C x ⟼ x 2 nd ⁡ f y ⁡ g ⁡ u = g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ u
34 33 mpteq2dva ⊢ φ ∧ f = F ∧ x = X → y ∈ B ⟼ g ∈ y Hom ⁡ C x ⟼ x 2 nd ⁡ f y ⁡ g ⁡ u = y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ u
35 24 34 mpteq12dv ⊢ φ ∧ f = F ∧ x = X → u ∈ 1 st ⁡ f ⁡ x ⟼ y ∈ B ⟼ g ∈ y Hom ⁡ C x ⟼ x 2 nd ⁡ f y ⁡ g ⁡ u = u ∈ 1 st ⁡ F ⁡ X ⟼ y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ u
36 fvex ⊢ 1 st ⁡ F ⁡ X ∈ V
37 36 mptex ⊢ u ∈ 1 st ⁡ F ⁡ X ⟼ y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ u ∈ V
38 37 a1i ⊢ φ → u ∈ 1 st ⁡ F ⁡ X ⟼ y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ u ∈ V
39 20 35 16 17 38 ovmpod ⊢ φ → F N X = u ∈ 1 st ⁡ F ⁡ X ⟼ y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ u
40 simpr ⊢ φ ∧ u = A → u = A
41 40 fveq2d ⊢ φ ∧ u = A → X 2 nd ⁡ F y ⁡ g ⁡ u = X 2 nd ⁡ F y ⁡ g ⁡ A
42 41 mpteq2dv ⊢ φ ∧ u = A → g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ u = g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A
43 42 mpteq2dv ⊢ φ ∧ u = A → y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ u = y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A
44 2 fvexi ⊢ B ∈ V
45 44 mptex ⊢ y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A ∈ V
46 45 a1i ⊢ φ → y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A ∈ V
47 39 43 19 46 fvmptd ⊢ φ → F N X ⁡ A = y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A