Metamath Proof Explorer

Theorem oppcup

Description: The universal pair <. X , M >. from a functor to an object is universal from an object to a functor in the opposite category. (Contributed by Zhi Wang, 24-Sep-2025)

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

Proof

Step Hyp Ref Expression
1 oppcup.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
2 oppcup.c ⊢ 𝐶 = ( Base ‘ 𝐸 )
3 oppcup.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
4 oppcup.j ⊢ 𝐽 = ( Hom ‘ 𝐸 )
5 oppcup.xb ⊢ ∙ = ( comp ‘ 𝐸 )
6 oppcup.w ⊢ ( 𝜑 → 𝑊 ∈ 𝐶 )
7 oppcup.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
8 oppcup.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
9 oppcup.m ⊢ ( 𝜑 → 𝑀 ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 𝑊 ) )
10 oppcup.o ⊢ 𝑂 = ( oppCat ‘ 𝐷 )
11 oppcup.p ⊢ 𝑃 = ( oppCat ‘ 𝐸 )
12 10 1 oppcbas ⊢ 𝐵 = ( Base ‘ 𝑂 )
13 11 2 oppcbas ⊢ 𝐶 = ( Base ‘ 𝑃 )
14 eqid ⊢ ( Hom ‘ 𝑂 ) = ( Hom ‘ 𝑂 )
15 eqid ⊢ ( Hom ‘ 𝑃 ) = ( Hom ‘ 𝑃 )
16 eqid ⊢ ( comp ‘ 𝑃 ) = ( comp ‘ 𝑃 )
17 10 11 7 funcoppc ⊢ ( 𝜑 → 𝐹 ( 𝑂 Func 𝑃 ) tpos 𝐺 )
18 4 11 oppchom ⊢ ( 𝑊 ( Hom ‘ 𝑃 ) ( 𝐹 ‘ 𝑋 ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝐽 𝑊 )
19 9 18 eleqtrrdi ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑊 ( Hom ‘ 𝑃 ) ( 𝐹 ‘ 𝑋 ) ) )
20 12 13 14 15 16 6 17 8 19 isup ⊢ ( 𝜑 → ( 𝑋 ( ⟨ 𝐹 , tpos 𝐺 ⟩ ( 𝑂 UP 𝑃 ) 𝑊 ) 𝑀 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 ( Hom ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑦 ) 𝑔 = ( ( ( 𝑋 tpos 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) ) )
21 4 11 oppchom ⊢ ( 𝑊 ( Hom ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑦 ) 𝐽 𝑊 )
22 21 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑊 ( Hom ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑦 ) 𝐽 𝑊 ) )
23 3 10 oppchom ⊢ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑦 ) = ( 𝑦 𝐻 𝑋 )
24 23 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑋 ( Hom ‘ 𝑂 ) 𝑦 ) = ( 𝑦 𝐻 𝑋 ) )
25 ovtpos ⊢ ( 𝑋 tpos 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑋 )
26 25 fveq1i ⊢ ( ( 𝑋 tpos 𝐺 𝑦 ) ‘ 𝑘 ) = ( ( 𝑦 𝐺 𝑋 ) ‘ 𝑘 )
27 26 oveq1i ⊢ ( ( ( 𝑋 tpos 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) = ( ( ( 𝑦 𝐺 𝑋 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) 𝑀 )
28 6 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑊 ∈ 𝐶 )
29 7 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
30 1 2 29 funcf1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐹 : 𝐵 ⟶ 𝐶 )
31 8 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
32 30 31 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐶 )
33 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
34 30 33 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐶 )
35 2 5 11 28 32 34 oppcco ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( ( 𝑦 𝐺 𝑋 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) = ( 𝑀 ( ⟨ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ∙ 𝑊 ) ( ( 𝑦 𝐺 𝑋 ) ‘ 𝑘 ) ) )
36 27 35 eqtrid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ( ( 𝑋 tpos 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) = ( 𝑀 ( ⟨ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ∙ 𝑊 ) ( ( 𝑦 𝐺 𝑋 ) ‘ 𝑘 ) ) )
37 36 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑔 = ( ( ( 𝑋 tpos 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) ↔ 𝑔 = ( 𝑀 ( ⟨ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ∙ 𝑊 ) ( ( 𝑦 𝐺 𝑋 ) ‘ 𝑘 ) ) ) )
38 24 37 reueqbidv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ∃! 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑦 ) 𝑔 = ( ( ( 𝑋 tpos 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) ↔ ∃! 𝑘 ∈ ( 𝑦 𝐻 𝑋 ) 𝑔 = ( 𝑀 ( ⟨ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ∙ 𝑊 ) ( ( 𝑦 𝐺 𝑋 ) ‘ 𝑘 ) ) ) )
39 22 38 raleqbidv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ∀ 𝑔 ∈ ( 𝑊 ( Hom ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑦 ) 𝑔 = ( ( ( 𝑋 tpos 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) ↔ ∀ 𝑔 ∈ ( ( 𝐹 ‘ 𝑦 ) 𝐽 𝑊 ) ∃! 𝑘 ∈ ( 𝑦 𝐻 𝑋 ) 𝑔 = ( 𝑀 ( ⟨ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ∙ 𝑊 ) ( ( 𝑦 𝐺 𝑋 ) ‘ 𝑘 ) ) ) )
40 39 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑊 ( Hom ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑦 ) 𝑔 = ( ( ( 𝑋 tpos 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( ( 𝐹 ‘ 𝑦 ) 𝐽 𝑊 ) ∃! 𝑘 ∈ ( 𝑦 𝐻 𝑋 ) 𝑔 = ( 𝑀 ( ⟨ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ∙ 𝑊 ) ( ( 𝑦 𝐺 𝑋 ) ‘ 𝑘 ) ) ) )
41 20 40 bitrd ⊢ ( 𝜑 → ( 𝑋 ( ⟨ 𝐹 , tpos 𝐺 ⟩ ( 𝑂 UP 𝑃 ) 𝑊 ) 𝑀 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( ( 𝐹 ‘ 𝑦 ) 𝐽 𝑊 ) ∃! 𝑘 ∈ ( 𝑦 𝐻 𝑋 ) 𝑔 = ( 𝑀 ( ⟨ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑋 ) ⟩ ∙ 𝑊 ) ( ( 𝑦 𝐺 𝑋 ) ‘ 𝑘 ) ) ) )