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	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( ( 𝐹 ‘ 𝑦 ) 𝐽 𝑊 ) ∃! 𝑘 ∈ ( 𝑦 𝐻 𝑋 ) 𝑔 = ( 𝑀 ( ⟨ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ∙ 𝑊 ) ( ( 𝑦 𝐺 𝑋 ) ‘ 𝑘 ) ) )