isup2

Description: The universal property of a universal pair. (Contributed by Zhi Wang, 24-Sep-2025)

	Ref	Expression
Hypotheses	isup2.b	$⊢ B = {Base}_{D}$
	isup2.h	$⊢ H = Hom (D)$
	isup2.j	$⊢ J = Hom (E)$
	isup2.o	$⊢ O = comp (E)$
	isup2.x	No typesetting found for \|- ( ph -> X ( <. F , G >. ( D UP E ) W ) M ) with typecode \|-
Assertion	isup2	$⊢ φ \to \forall y \in B \forall g \in (W J F (y)) \exists! k \in (X H y) g = (X G y) (k) (⟨W, F (X)⟩ O F (y)) M$

Step	Hyp	Ref	Expression
1		isup2.b	$⊢ B = {Base}_{D}$
2		isup2.h	$⊢ H = Hom (D)$
3		isup2.j	$⊢ J = Hom (E)$
4		isup2.o	$⊢ O = comp (E)$
5		isup2.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 \|-
6		eqid	$⊢ {Base}_{E} = {Base}_{E}$
7	5 6	uprcl3	$⊢ φ \to W \in {Base}_{E}$
8	5	uprcl2	$⊢ φ \to F (D Func E) G$
9	5 1	uprcl4	$⊢ φ \to X \in B$
10	5 3	uprcl5	$⊢ φ \to M \in (W J F (X))$
11	1 6 2 3 4 7 8 9 10	isup	Could not format ( ph -> ( X ( <. F , G >. ( D UP E ) W ) M <-> A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( X H y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) M ) ) ) : No typesetting found for \|- ( ph -> ( X ( <. F , G >. ( D UP E ) W ) M <-> A. y e. B A. g e. ( W J ( F ` y ) ) E! k e. ( X H y ) g = ( ( ( X G y ) ` k ) ( <. W , ( F ` X ) >. O ( F ` y ) ) M ) ) ) with typecode \|-
12	5 11	mpbid	$⊢ φ \to \forall y \in B \forall g \in (W J F (y)) \exists! k \in (X H y) g = (X G y) (k) (⟨W, F (X)⟩ O F (y)) M$

Metamath Proof Explorer