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

Metamath Proof Explorer

Theorem oppcup2

Description: The universal property for the universal pair <. X , M >. from a functor to an object, expressed explicitly. (Contributed by Zhi Wang, 4-Nov-2025)

Ref Expression
Hypotheses oppcup2.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
oppcup2.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
oppcup2.j ⊢ 𝐽 = ( Hom ‘ 𝐸 )
oppcup2.xb ⊢ ∙ = ( comp ‘ 𝐸 )
oppcup2.o ⊢ 𝑂 = ( oppCat ‘ 𝐷 )
oppcup2.p ⊢ 𝑃 = ( oppCat ‘ 𝐸 )
oppcup2.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
oppcup2.x ⊢ ( 𝜑 → 𝑋 ( ⟨ 𝐹 , tpos 𝐺 ⟩ ( 𝑂 UP 𝑃 ) 𝑊 ) 𝑀 )
Assertion oppcup2 ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( ( 𝐹 ‘ 𝑦 ) 𝐽 𝑊 ) ∃! 𝑘 ∈ ( 𝑦 𝐻 𝑋 ) 𝑔 = ( 𝑀 ( ⟨ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ∙ 𝑊 ) ( ( 𝑦 𝐺 𝑋 ) ‘ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 oppcup2.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
2 oppcup2.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
3 oppcup2.j ⊢ 𝐽 = ( Hom ‘ 𝐸 )
4 oppcup2.xb ⊢ ∙ = ( comp ‘ 𝐸 )
5 oppcup2.o ⊢ 𝑂 = ( oppCat ‘ 𝐷 )
6 oppcup2.p ⊢ 𝑃 = ( oppCat ‘ 𝐸 )
7 oppcup2.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
8 oppcup2.x ⊢ ( 𝜑 → 𝑋 ( ⟨ 𝐹 , tpos 𝐺 ⟩ ( 𝑂 UP 𝑃 ) 𝑊 ) 𝑀 )
9 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
10 8 6 9 oppcuprcl3 ⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐸 ) )
11 8 5 1 oppcuprcl4 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
12 8 6 3 oppcuprcl5 ⊢ ( 𝜑 → 𝑀 ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 𝑊 ) )
13 1 9 2 3 4 10 7 11 12 5 6 oppcup ⊢ ( 𝜑 → ( 𝑋 ( ⟨ 𝐹 , tpos 𝐺 ⟩ ( 𝑂 UP 𝑃 ) 𝑊 ) 𝑀 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( ( 𝐹 ‘ 𝑦 ) 𝐽 𝑊 ) ∃! 𝑘 ∈ ( 𝑦 𝐻 𝑋 ) 𝑔 = ( 𝑀 ( ⟨ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ∙ 𝑊 ) ( ( 𝑦 𝐺 𝑋 ) ‘ 𝑘 ) ) ) )
14 8 13 mpbid ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( ( 𝐹 ‘ 𝑦 ) 𝐽 𝑊 ) ∃! 𝑘 ∈ ( 𝑦 𝐻 𝑋 ) 𝑔 = ( 𝑀 ( ⟨ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ∙ 𝑊 ) ( ( 𝑦 𝐺 𝑋 ) ‘ 𝑘 ) ) )