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

Metamath Proof Explorer

Theorem functermc2

Description: Functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025)

Ref Expression
Hypotheses functermc.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
functermc.e ⊢ ( 𝜑 → 𝐸 ∈ TermCat )
functermc.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
functermc.c ⊢ 𝐶 = ( Base ‘ 𝐸 )
functermc.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
functermc.j ⊢ 𝐽 = ( Hom ‘ 𝐸 )
functermc.f ⊢ 𝐹 = ( 𝐵 × 𝐶 )
functermc.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
Assertion functermc2 ( 𝜑 → ( 𝐷 Func 𝐸 ) = { ⟨ 𝐹 , 𝐺 ⟩ } )

Proof

Step Hyp Ref Expression
1 functermc.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
2 functermc.e ⊢ ( 𝜑 → 𝐸 ∈ TermCat )
3 functermc.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
4 functermc.c ⊢ 𝐶 = ( Base ‘ 𝐸 )
5 functermc.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
6 functermc.j ⊢ 𝐽 = ( Hom ‘ 𝐸 )
7 functermc.f ⊢ 𝐹 = ( 𝐵 × 𝐶 )
8 functermc.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
9 relfunc ⊢ Rel ( 𝐷 Func 𝐸 )
10 3 fvexi ⊢ 𝐵 ∈ V
11 4 fvexi ⊢ 𝐶 ∈ V
12 10 11 xpex ⊢ ( 𝐵 × 𝐶 ) ∈ V
13 7 12 eqeltri ⊢ 𝐹 ∈ V
14 10 10 mpoex ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ) ∈ V
15 8 14 eqeltri ⊢ 𝐺 ∈ V
16 13 15 relsnop ⊢ Rel { ⟨ 𝐹 , 𝐺 ⟩ }
17 1 2 3 4 5 6 7 8 functermc ⊢ ( 𝜑 → ( 𝑧 ( 𝐷 Func 𝐸 ) 𝑤 ↔ ( 𝑧 = 𝐹 ∧ 𝑤 = 𝐺 ) ) )
18 brsnop ⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝑧 { ⟨ 𝐹 , 𝐺 ⟩ } 𝑤 ↔ ( 𝑧 = 𝐹 ∧ 𝑤 = 𝐺 ) ) )
19 13 15 18 mp2an ⊢ ( 𝑧 { ⟨ 𝐹 , 𝐺 ⟩ } 𝑤 ↔ ( 𝑧 = 𝐹 ∧ 𝑤 = 𝐺 ) )
20 17 19 bitr4di ⊢ ( 𝜑 → ( 𝑧 ( 𝐷 Func 𝐸 ) 𝑤 ↔ 𝑧 { ⟨ 𝐹 , 𝐺 ⟩ } 𝑤 ) )
21 9 16 20 eqbrrdiv ⊢ ( 𝜑 → ( 𝐷 Func 𝐸 ) = { ⟨ 𝐹 , 𝐺 ⟩ } )