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

Metamath Proof Explorer

Theorem 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 ⊢ B = Base D
oppcup3.h ⊢ H = Hom ⁡ D
oppcup3.j ⊢ J = Hom ⁡ E
oppcup3.xb ⊢ ∙ ˙ = comp ⁡ E
oppcup3.o ⊢ O = oppCat ⁡ D
oppcup3.p ⊢ P = oppCat ⁡ E
oppcup3.x No typesetting found for |- ( ph -> X ( <. F , T >. ( O UP P ) W ) M ) with typecode |-
oppcup3.g ⊢ φ → tpos T = G
oppcup3.y ⊢ φ → Y ∈ B
oppcup3.n ⊢ φ → N ∈ F ⁡ Y J W
Assertion oppcup3 ⊢ φ → ∃! k ∈ Y H X N = M F ⁡ Y F ⁡ X ∙ ˙ W Y G X ⁡ k

Proof

Step Hyp Ref Expression
1 oppcup3.b ⊢ B = Base D
2 oppcup3.h ⊢ H = Hom ⁡ D
3 oppcup3.j ⊢ J = Hom ⁡ E
4 oppcup3.xb ⊢ ∙ ˙ = comp ⁡ E
5 oppcup3.o ⊢ O = oppCat ⁡ D
6 oppcup3.p ⊢ P = oppCat ⁡ E
7 oppcup3.x Could not format ( ph -> X ( <. F , T >. ( O UP P ) W ) M ) : No typesetting found for |- ( ph -> X ( <. F , T >. ( O UP P ) W ) M ) with typecode |-
8 oppcup3.g ⊢ φ → tpos T = G
9 oppcup3.y ⊢ φ → Y ∈ B
10 oppcup3.n ⊢ φ → N ∈ F ⁡ Y J W
11 9 1 eleqtrdi ⊢ φ → Y ∈ Base D
12 11 elfvexd ⊢ φ → D ∈ V
13 10 ne0d ⊢ φ → F ⁡ Y J W ≠ ∅
14 fvprc ⊢ ¬ E ∈ V → Hom ⁡ E = ∅
15 3 14 eqtrid ⊢ ¬ E ∈ V → J = ∅
16 15 oveqd ⊢ ¬ E ∈ V → F ⁡ Y J W = F ⁡ Y ∅ W
17 0ov ⊢ F ⁡ Y ∅ W = ∅
18 16 17 eqtrdi ⊢ ¬ E ∈ V → F ⁡ Y J W = ∅
19 18 necon1ai ⊢ F ⁡ Y J W ≠ ∅ → E ∈ V
20 13 19 syl ⊢ φ → E ∈ V
21 7 6 5 12 20 8 oppcuprcl2 ⊢ φ → F D Func E G
22 7 8 uptpos Could not format ( ph -> X ( <. F , tpos G >. ( O UP P ) W ) M ) : No typesetting found for |- ( ph -> X ( <. F , tpos G >. ( O UP P ) W ) M ) with typecode |-
23 1 2 3 4 5 6 21 22 oppcup2 ⊢ φ → ∀ y ∈ B ∀ g ∈ F ⁡ y J W ∃! k ∈ y H X g = M F ⁡ y F ⁡ X ∙ ˙ W y G X ⁡ k
24 23 9 10 oppcup3lem ⊢ φ → ∃! k ∈ Y H X N = M F ⁡ Y F ⁡ X ∙ ˙ W Y G X ⁡ k