This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐼 = ( idfunc ‘ 𝐷 )
cofidval.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
cofidval.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
cofidval.k ⊢ ( 𝜑 → 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 )
cofidval.o ⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐼 )
cofidval.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
Assertion cofidval ( 𝜑 → ( ( 𝐾 ∘ 𝐹 ) = ( I ↾ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) = ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cofidval.i ⊢ 𝐼 = ( idfunc ‘ 𝐷 )
2 cofidval.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
3 cofidval.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
4 cofidval.k ⊢ ( 𝜑 → 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 )
5 cofidval.o ⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐼 )
6 cofidval.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
7 2 3 4 cofuval2 ⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝐾 ∘ 𝐹 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) ⟩ )
8 3 funcrcl2 ⊢ ( 𝜑 → 𝐷 ∈ Cat )
9 1 2 8 6 idfuval ⊢ ( 𝜑 → 𝐼 = ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ )
10 5 7 9 3eqtr3d ⊢ ( 𝜑 → ⟨ ( 𝐾 ∘ 𝐹 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) ⟩ = ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ )
11 2 fvexi ⊢ 𝐵 ∈ V
12 resiexg ⊢ ( 𝐵 ∈ V → ( I ↾ 𝐵 ) ∈ V )
13 11 12 ax-mp ⊢ ( I ↾ 𝐵 ) ∈ V
14 11 11 xpex ⊢ ( 𝐵 × 𝐵 ) ∈ V
15 14 mptex ⊢ ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ∈ V
16 13 15 opth2 ⊢ ( ⟨ ( 𝐾 ∘ 𝐹 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) ⟩ = ⟨ ( I ↾ 𝐵 ) , ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ⟩ ↔ ( ( 𝐾 ∘ 𝐹 ) = ( I ↾ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) = ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ) )
17 10 16 sylib ⊢ ( 𝜑 → ( ( 𝐾 ∘ 𝐹 ) = ( I ↾ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) = ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( 𝐻 ‘ 𝑧 ) ) ) ) )