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

Metamath Proof Explorer

Theorem uprcl4

Description: Reverse closure for the class of universal property. (Contributed by Zhi Wang, 25-Sep-2025)

Ref Expression
Hypotheses uprcl2.x No typesetting found for |- ( ph -> X ( <. F , G >. ( D UP E ) W ) M ) with typecode |-
uprcl4.b ⊢ B = Base D
Assertion uprcl4 ⊢ φ → X ∈ B

Proof

Step Hyp Ref Expression
1 uprcl2.x Could not format ( ph -> X ( <. F , G >. ( D UP E ) W ) M ) : No typesetting found for |- ( ph -> X ( <. F , G >. ( D UP E ) W ) M ) with typecode |-
2 uprcl4.b ⊢ B = Base D
3 eqid ⊢ Base E = Base E
4 eqid ⊢ Hom ⁡ D = Hom ⁡ D
5 eqid ⊢ Hom ⁡ E = Hom ⁡ E
6 eqid ⊢ comp ⁡ E = comp ⁡ E
7 1 3 uprcl3 ⊢ φ → W ∈ Base E
8 1 uprcl2 ⊢ φ → F D Func E G
9 2 3 4 5 6 7 8 isuplem Could not format ( ph -> ( X ( <. F , G >. ( D UP E ) W ) M <-> ( ( X e. B /\ M e. ( W ( Hom ` E ) ( F ` X ) ) ) /\ A. y e. B A. g e. ( W ( Hom ` E ) ( F ` y ) ) E! k e. ( X ( Hom ` D ) y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` y ) ) M ) ) ) ) : No typesetting found for |- ( ph -> ( X ( <. F , G >. ( D UP E ) W ) M <-> ( ( X e. B /\ M e. ( W ( Hom ` E ) ( F ` X ) ) ) /\ A. y e. B A. g e. ( W ( Hom ` E ) ( F ` y ) ) E! k e. ( X ( Hom ` D ) y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. ( comp ` E ) ( F ` y ) ) M ) ) ) ) with typecode |-
10 1 9 mpbid ⊢ φ → X ∈ B ∧ M ∈ W Hom ⁡ E F ⁡ X ∧ ∀ y ∈ B ∀ g ∈ W Hom ⁡ E F ⁡ y ∃! k ∈ X Hom ⁡ D y g = X G y ⁡ k W F ⁡ X comp ⁡ E F ⁡ y M
11 10 simplld ⊢ φ → X ∈ B