Metamath Proof Explorer

Theorem cofidvala

Description: The property " F is a section of G " in a category of small categories (in a universe); expressed explicitly. (Contributed by Zhi Wang, 15-Nov-2025)

Ref Expression
Hypotheses cofidvala.i ⊢ I = id func ⁡ D
cofidvala.b ⊢ B = Base D
cofidvala.f ⊢ φ → F ∈ D Func E
cofidvala.g ⊢ φ → G ∈ E Func D
cofidvala.o ⊢ φ → G ∘ func F = I
cofidvala.h ⊢ H = Hom ⁡ D
Assertion cofidvala ⊢ φ → 1 st ⁡ G ∘ 1 st ⁡ F = I ↾ B ∧ x ∈ B , y ∈ B ⟼ 1 st ⁡ F ⁡ x 2 nd ⁡ G 1 st ⁡ F ⁡ y ∘ x 2 nd ⁡ F y = z ∈ B × B ⟼ I ↾ H ⁡ z

Proof

Step Hyp Ref Expression
1 cofidvala.i ⊢ I = id func ⁡ D
2 cofidvala.b ⊢ B = Base D
3 cofidvala.f ⊢ φ → F ∈ D Func E
4 cofidvala.g ⊢ φ → G ∈ E Func D
5 cofidvala.o ⊢ φ → G ∘ func F = I
6 cofidvala.h ⊢ H = Hom ⁡ D
7 2 3 4 cofuval ⊢ φ → G ∘ func F = 1 st ⁡ G ∘ 1 st ⁡ F x ∈ B , y ∈ B ⟼ 1 st ⁡ F ⁡ x 2 nd ⁡ G 1 st ⁡ F ⁡ y ∘ x 2 nd ⁡ F y
8 3 func1st2nd ⊢ φ → 1 st ⁡ F D Func E 2 nd ⁡ F
9 8 funcrcl2 ⊢ φ → D ∈ Cat
10 1 2 9 6 idfuval ⊢ φ → I = I ↾ B z ∈ B × B ⟼ I ↾ H ⁡ z
11 5 7 10 3eqtr3d ⊢ φ → 1 st ⁡ G ∘ 1 st ⁡ F x ∈ B , y ∈ B ⟼ 1 st ⁡ F ⁡ x 2 nd ⁡ G 1 st ⁡ F ⁡ y ∘ x 2 nd ⁡ F y = I ↾ B z ∈ B × B ⟼ I ↾ H ⁡ z
12 2 fvexi ⊢ B ∈ V
13 resiexg ⊢ B ∈ V → I ↾ B ∈ V
14 12 13 ax-mp ⊢ I ↾ B ∈ V
15 12 12 xpex ⊢ B × B ∈ V
16 15 mptex ⊢ z ∈ B × B ⟼ I ↾ H ⁡ z ∈ V
17 14 16 opth2 ⊢ 1 st ⁡ G ∘ 1 st ⁡ F x ∈ B , y ∈ B ⟼ 1 st ⁡ F ⁡ x 2 nd ⁡ G 1 st ⁡ F ⁡ y ∘ x 2 nd ⁡ F y = I ↾ B z ∈ B × B ⟼ I ↾ H ⁡ z ↔ 1 st ⁡ G ∘ 1 st ⁡ F = I ↾ B ∧ x ∈ B , y ∈ B ⟼ 1 st ⁡ F ⁡ x 2 nd ⁡ G 1 st ⁡ F ⁡ y ∘ x 2 nd ⁡ F y = z ∈ B × B ⟼ I ↾ H ⁡ z
18 11 17 sylib ⊢ φ → 1 st ⁡ G ∘ 1 st ⁡ F = I ↾ B ∧ x ∈ B , y ∈ B ⟼ 1 st ⁡ F ⁡ x 2 nd ⁡ G 1 st ⁡ F ⁡ y ∘ x 2 nd ⁡ F y = z ∈ B × B ⟼ I ↾ H ⁡ z