Theorem oppcuprcl2

Description: Reverse closure for the class of universal property in opposite categories. (Contributed by Zhi Wang, 4-Nov-2025)

	Ref	Expression
Hypotheses	oppcuprcl2.x	⊢ ( 𝜑 → 𝑋 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝑂 UP 𝑃 ) 𝑊 ) 𝑀 )
	oppcuprcl2.p	⊢ 𝑃 = ( oppCat ‘ 𝐸 )
	oppcuprcl2.o	⊢ 𝑂 = ( oppCat ‘ 𝐷 )
	oppcuprcl2.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
	oppcuprcl2.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
	oppcuprcl2.h	⊢ ( 𝜑 → tpos 𝐺 = 𝐻 )
Assertion	oppcuprcl2	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		oppcuprcl2.x	⊢ ( 𝜑 → 𝑋 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝑂 UP 𝑃 ) 𝑊 ) 𝑀 )
2		oppcuprcl2.p	⊢ 𝑃 = ( oppCat ‘ 𝐸 )
3		oppcuprcl2.o	⊢ 𝑂 = ( oppCat ‘ 𝐷 )
4		oppcuprcl2.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
5		oppcuprcl2.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
6		oppcuprcl2.h	⊢ ( 𝜑 → tpos 𝐺 = 𝐻 )
7	1	uprcl2	⊢ ( 𝜑 → 𝐹 ( 𝑂 Func 𝑃 ) 𝐺 )
8	3 2 4 5 7	funcoppc2	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) tpos 𝐺 )
9	8 6	breqtrd	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐻 )