oppcup3

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	oppcup3.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	oppcup3.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
	oppcup3.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
	oppcup3.xb	⊢ ∙ = ( comp ‘ 𝐸 )
	oppcup3.o	⊢ 𝑂 = ( oppCat ‘ 𝐷 )
	oppcup3.p	⊢ 𝑃 = ( oppCat ‘ 𝐸 )
	oppcup3.x	⊢ ( 𝜑 → 𝑋 ( ⟨ 𝐹 , 𝑇 ⟩ ( 𝑂 UP 𝑃 ) 𝑊 ) 𝑀 )
	oppcup3.g	⊢ ( 𝜑 → tpos 𝑇 = 𝐺 )
	oppcup3.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	oppcup3.n	⊢ ( 𝜑 → 𝑁 ∈ ( ( 𝐹 ‘ 𝑌 ) 𝐽 𝑊 ) )
Assertion	oppcup3	⊢ ( 𝜑 → ∃! 𝑘 ∈ ( 𝑌 𝐻 𝑋 ) 𝑁 = ( 𝑀 ( ⟨ ( 𝐹 ‘ 𝑌 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ∙ 𝑊 ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑘 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oppcup3.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
2		oppcup3.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
3		oppcup3.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
4		oppcup3.xb	⊢ ∙ = ( comp ‘ 𝐸 )
5		oppcup3.o	⊢ 𝑂 = ( oppCat ‘ 𝐷 )
6		oppcup3.p	⊢ 𝑃 = ( oppCat ‘ 𝐸 )
7		oppcup3.x	⊢ ( 𝜑 → 𝑋 ( ⟨ 𝐹 , 𝑇 ⟩ ( 𝑂 UP 𝑃 ) 𝑊 ) 𝑀 )
8		oppcup3.g	⊢ ( 𝜑 → tpos 𝑇 = 𝐺 )
9		oppcup3.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
10		oppcup3.n	⊢ ( 𝜑 → 𝑁 ∈ ( ( 𝐹 ‘ 𝑌 ) 𝐽 𝑊 ) )
11	9 1	eleqtrdi	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐷 ) )
12	11	elfvexd	⊢ ( 𝜑 → 𝐷 ∈ V )
13	10	ne0d	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑌 ) 𝐽 𝑊 ) ≠ ∅ )
14		fvprc	⊢ ( ¬ 𝐸 ∈ V → ( Hom ‘ 𝐸 ) = ∅ )
15	3 14	eqtrid	⊢ ( ¬ 𝐸 ∈ V → 𝐽 = ∅ )
16	15	oveqd	⊢ ( ¬ 𝐸 ∈ V → ( ( 𝐹 ‘ 𝑌 ) 𝐽 𝑊 ) = ( ( 𝐹 ‘ 𝑌 ) ∅ 𝑊 ) )
17		0ov	⊢ ( ( 𝐹 ‘ 𝑌 ) ∅ 𝑊 ) = ∅
18	16 17	eqtrdi	⊢ ( ¬ 𝐸 ∈ V → ( ( 𝐹 ‘ 𝑌 ) 𝐽 𝑊 ) = ∅ )
19	18	necon1ai	⊢ ( ( ( 𝐹 ‘ 𝑌 ) 𝐽 𝑊 ) ≠ ∅ → 𝐸 ∈ V )
20	13 19	syl	⊢ ( 𝜑 → 𝐸 ∈ V )
21	7 6 5 12 20 8	oppcuprcl2	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
22	7 8	uptpos	⊢ ( 𝜑 → 𝑋 ( ⟨ 𝐹 , tpos 𝐺 ⟩ ( 𝑂 UP 𝑃 ) 𝑊 ) 𝑀 )
23	1 2 3 4 5 6 21 22	oppcup2	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( ( 𝐹 ‘ 𝑦 ) 𝐽 𝑊 ) ∃! 𝑘 ∈ ( 𝑦 𝐻 𝑋 ) 𝑔 = ( 𝑀 ( ⟨ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ∙ 𝑊 ) ( ( 𝑦 𝐺 𝑋 ) ‘ 𝑘 ) ) )
24	23 9 10	oppcup3lem	⊢ ( 𝜑 → ∃! 𝑘 ∈ ( 𝑌 𝐻 𝑋 ) 𝑁 = ( 𝑀 ( ⟨ ( 𝐹 ‘ 𝑌 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ∙ 𝑊 ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑘 ) ) )

Metamath Proof Explorer

Theorem oppcup3

Proof