Metamath Proof Explorer

Theorem cofidval

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

Ref Expression
Hypotheses cofidval.i ⊢ I = id func ⁡ D
cofidval.b ⊢ B = Base D
cofidval.f ⊢ φ → F D Func E G
cofidval.k ⊢ φ → K E Func D L
cofidval.o ⊢ φ → K L ∘ func F G = I
cofidval.h ⊢ H = Hom ⁡ D
Assertion cofidval ⊢ φ → K ∘ F = I ↾ B ∧ x ∈ B , y ∈ B ⟼ F ⁡ x L F ⁡ y ∘ x G y = z ∈ B × B ⟼ I ↾ H ⁡ z

Proof

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