Metamath Proof Explorer

Theorem yonedalem4b

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
yonedalem4b.p ⊢ φ → P ∈ B
yonedalem4b.g ⊢ φ → G ∈ P Hom ⁡ C X
Assertion yonedalem4b ⊢ φ → F N X ⁡ A ⁡ P ⁡ G = X 2 nd ⁡ F P ⁡ 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 yonedalem4b.p ⊢ φ → P ∈ B
21 yonedalem4b.g ⊢ φ → G ∈ P Hom ⁡ C X
22 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 yonedalem4a ⊢ φ → F N X ⁡ A = y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A
23 22 fveq1d ⊢ φ → F N X ⁡ A ⁡ P = y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A ⁡ P
24 23 fveq1d ⊢ φ → F N X ⁡ A ⁡ P ⁡ G = y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A ⁡ P ⁡ G
25 eqidd ⊢ φ → y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A = y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A
26 ovex ⊢ y Hom ⁡ C X ∈ V
27 26 mptex ⊢ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A ∈ V
28 27 a1i ⊢ φ ∧ y = P → g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A ∈ V
29 21 adantr ⊢ φ ∧ y = P → G ∈ P Hom ⁡ C X
30 simpr ⊢ φ ∧ y = P → y = P
31 30 oveq1d ⊢ φ ∧ y = P → y Hom ⁡ C X = P Hom ⁡ C X
32 29 31 eleqtrrd ⊢ φ ∧ y = P → G ∈ y Hom ⁡ C X
33 fvexd ⊢ φ ∧ y = P ∧ g = G → X 2 nd ⁡ F y ⁡ g ⁡ A ∈ V
34 simplr ⊢ φ ∧ y = P ∧ g = G → y = P
35 34 oveq2d ⊢ φ ∧ y = P ∧ g = G → X 2 nd ⁡ F y = X 2 nd ⁡ F P
36 simpr ⊢ φ ∧ y = P ∧ g = G → g = G
37 35 36 fveq12d ⊢ φ ∧ y = P ∧ g = G → X 2 nd ⁡ F y ⁡ g = X 2 nd ⁡ F P ⁡ G
38 37 fveq1d ⊢ φ ∧ y = P ∧ g = G → X 2 nd ⁡ F y ⁡ g ⁡ A = X 2 nd ⁡ F P ⁡ G ⁡ A
39 32 33 38 fvmptdv2 ⊢ φ ∧ y = P → y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A ⁡ P = g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A → y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A ⁡ P ⁡ G = X 2 nd ⁡ F P ⁡ G ⁡ A
40 nfmpt1 ⊢ Ⅎ _ y y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A
41 nffvmpt1 ⊢ Ⅎ _ y y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A ⁡ P
42 nfcv ⊢ Ⅎ _ y G
43 41 42 nffv ⊢ Ⅎ _ y y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A ⁡ P ⁡ G
44 43 nfeq1 ⊢ Ⅎ y y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A ⁡ P ⁡ G = X 2 nd ⁡ F P ⁡ G ⁡ A
45 20 28 39 40 44 fvmptd2f ⊢ φ → y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A = y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A → y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A ⁡ P ⁡ G = X 2 nd ⁡ F P ⁡ G ⁡ A
46 25 45 mpd ⊢ φ → y ∈ B ⟼ g ∈ y Hom ⁡ C X ⟼ X 2 nd ⁡ F y ⁡ g ⁡ A ⁡ P ⁡ G = X 2 nd ⁡ F P ⁡ G ⁡ A
47 24 46 eqtrd ⊢ φ → F N X ⁡ A ⁡ P ⁡ G = X 2 nd ⁡ F P ⁡ G ⁡ A