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

Metamath Proof Explorer

Theorem diag1f1olem

Description: To any functor from a terminal category can an object in the target base be assigned. (Contributed by Zhi Wang, 21-Oct-2025)

Ref Expression
Hypotheses diag1f1o.a ⊢ 𝐴 = ( Base ‘ 𝐶 )
diag1f1o.d ⊢ ( 𝜑 → 𝐷 ∈ TermCat )
termcfuncval.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐶 ) )
termcfuncval.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
termcfuncval.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
termcfuncval.x ⊢ 𝑋 = ( ( 1st ‘ 𝐾 ) ‘ 𝑌 )
diag1f1olem.l ⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
Assertion diag1f1olem ( 𝜑 → ( 𝑋 ∈ 𝐴 ∧ 𝐾 = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 diag1f1o.a ⊢ 𝐴 = ( Base ‘ 𝐶 )
2 diag1f1o.d ⊢ ( 𝜑 → 𝐷 ∈ TermCat )
3 termcfuncval.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐶 ) )
4 termcfuncval.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
5 termcfuncval.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 termcfuncval.x ⊢ 𝑋 = ( ( 1st ‘ 𝐾 ) ‘ 𝑌 )
7 diag1f1olem.l ⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
8 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
9 eqid ⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
10 1 2 3 4 5 6 8 9 termcfuncval ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐴 ∧ 𝐾 = ⟨ { ⟨ 𝑌 , 𝑋 ⟩ } , { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ⟩ } ⟩ ) )
11 10 simpld ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
12 2 4 5 termcbas2 ⊢ ( 𝜑 → 𝐵 = { 𝑌 } )
13 12 xpeq1d ⊢ ( 𝜑 → ( 𝐵 × { 𝑋 } ) = ( { 𝑌 } × { 𝑋 } ) )
14 xpsng ⊢ ( ( 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( { 𝑌 } × { 𝑋 } ) = { ⟨ 𝑌 , 𝑋 ⟩ } )
15 5 11 14 syl2anc ⊢ ( 𝜑 → ( { 𝑌 } × { 𝑋 } ) = { ⟨ 𝑌 , 𝑋 ⟩ } )
16 13 15 eqtrd ⊢ ( 𝜑 → ( 𝐵 × { 𝑋 } ) = { ⟨ 𝑌 , 𝑋 ⟩ } )
17 12 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐵 = { 𝑌 } )
18 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝐷 ∈ TermCat )
19 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
20 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑧 ∈ 𝐵 )
21 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
22 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
23 18 4 19 20 21 9 22 termchom2 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) = { ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) } )
24 23 xpeq1d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) = ( { ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) } × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) )
25 fvex ⊢ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) ∈ V
26 fvex ⊢ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∈ V
27 25 26 xpsn ⊢ ( { ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) } × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) = { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ }
28 24 27 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) = { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } )
29 12 17 28 mpoeq123dva ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) = ( 𝑦 ∈ { 𝑌 } , 𝑧 ∈ { 𝑌 } ↦ { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ) )
30 snex ⊢ { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ∈ V
31 30 a1i ⊢ ( 𝜑 → { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ∈ V )
32 eqid ⊢ ( 𝑦 ∈ { 𝑌 } , 𝑧 ∈ { 𝑌 } ↦ { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ) = ( 𝑦 ∈ { 𝑌 } , 𝑧 ∈ { 𝑌 } ↦ { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } )
33 eqidd ⊢ ( 𝑦 = 𝑌 → { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } = { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } )
34 eqidd ⊢ ( 𝑧 = 𝑌 → { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } = { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } )
35 32 33 34 mposn ⊢ ( ( 𝑌 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ∈ V ) → ( 𝑦 ∈ { 𝑌 } , 𝑧 ∈ { 𝑌 } ↦ { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ) = { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ⟩ } )
36 5 5 31 35 syl3anc ⊢ ( 𝜑 → ( 𝑦 ∈ { 𝑌 } , 𝑧 ∈ { 𝑌 } ↦ { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ) = { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ⟩ } )
37 29 36 eqtrd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) = { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ⟩ } )
38 16 37 opeq12d ⊢ ( 𝜑 → ⟨ ( 𝐵 × { 𝑋 } ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) ⟩ = ⟨ { ⟨ 𝑌 , 𝑋 ⟩ } , { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ⟩ } ⟩ )
39 3 func1st2nd ⊢ ( 𝜑 → ( 1st ‘ 𝐾 ) ( 𝐷 Func 𝐶 ) ( 2nd ‘ 𝐾 ) )
40 39 funcrcl3 ⊢ ( 𝜑 → 𝐶 ∈ Cat )
41 2 termccd ⊢ ( 𝜑 → 𝐷 ∈ Cat )
42 eqid ⊢ ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 )
43 7 40 41 1 11 42 4 21 8 diag1a ⊢ ( 𝜑 → ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) = ⟨ ( 𝐵 × { 𝑋 } ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) × { ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) } ) ) ⟩ )
44 10 simprd ⊢ ( 𝜑 → 𝐾 = ⟨ { ⟨ 𝑌 , 𝑋 ⟩ } , { ⟨ ⟨ 𝑌 , 𝑌 ⟩ , { ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ } ⟩ } ⟩ )
45 38 43 44 3eqtr4rd ⊢ ( 𝜑 → 𝐾 = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) )
46 11 45 jca ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐴 ∧ 𝐾 = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) ) )