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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 oppcup2.b ⊢ B = Base D
2 oppcup2.h ⊢ H = Hom ⁡ D
3 oppcup2.j ⊢ J = Hom ⁡ E
4 oppcup2.xb ⊢ ∙ ˙ = comp ⁡ E
5 oppcup2.o ⊢ O = oppCat ⁡ D
6 oppcup2.p ⊢ P = oppCat ⁡ E
7 oppcup2.f ⊢ φ → F D Func E G
8 oppcup2.x 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 |-
9 eqid ⊢ Base E = Base E
10 8 6 9 oppcuprcl3 ⊢ φ → W ∈ Base E
11 8 5 1 oppcuprcl4 ⊢ φ → X ∈ B
12 8 6 3 oppcuprcl5 ⊢ φ → M ∈ F ⁡ X J W
13 1 9 2 3 4 10 7 11 12 5 6 oppcup Could not format ( ph -> ( X ( <. F , tpos G >. ( O UP P ) W ) M <-> A. y e. B A. g e. ( ( F ` y ) J W ) E! k e. ( y H X ) g = ( M ( <. ( F ` y ) , ( F ` X ) >. .xb W ) ( ( y G X ) ` k ) ) ) ) : No typesetting found for |- ( ph -> ( X ( <. F , tpos G >. ( O UP P ) W ) M <-> A. y e. B A. g e. ( ( F ` y ) J W ) E! k e. ( y H X ) g = ( M ( <. ( F ` y ) , ( F ` X ) >. .xb W ) ( ( y G X ) ` k ) ) ) ) with typecode |-
14 8 13 mpbid ⊢ φ → ∀ y ∈ B ∀ g ∈ F ⁡ y J W ∃! k ∈ y H X g = M F ⁡ y F ⁡ X ∙ ˙ W y G X ⁡ k