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

Metamath Proof Explorer

Theorem relup

Description: The set of universal pairs is a relation. (Contributed by Zhi Wang, 25-Sep-2025)

Ref Expression
Assertion relup Could not format assertion : No typesetting found for |- Rel ( F ( D UP E ) W ) with typecode |-

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base D = Base D
2 eqid ⊢ Base E = Base E
3 eqid ⊢ Hom ⁡ D = Hom ⁡ D
4 eqid ⊢ Hom ⁡ E = Hom ⁡ E
5 eqid ⊢ comp ⁡ E = comp ⁡ E
6 1 2 3 4 5 upfval Could not format ( D UP E ) = ( f e. ( D Func E ) , w e. ( Base ` E ) |-> { <. x , m >. | ( ( x e. ( Base ` D ) /\ m e. ( w ( Hom ` E ) ( ( 1st ` f ) ` x ) ) ) /\ A. y e. ( Base ` D ) A. g e. ( w ( Hom ` E ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` D ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` E ) ( ( 1st ` f ) ` y ) ) m ) ) } ) : No typesetting found for |- ( D UP E ) = ( f e. ( D Func E ) , w e. ( Base ` E ) |-> { <. x , m >. | ( ( x e. ( Base ` D ) /\ m e. ( w ( Hom ` E ) ( ( 1st ` f ) ` x ) ) ) /\ A. y e. ( Base ` D ) A. g e. ( w ( Hom ` E ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` D ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` E ) ( ( 1st ` f ) ` y ) ) m ) ) } ) with typecode |-
7 6 relmpoopab Could not format Rel ( F ( D UP E ) W ) : No typesetting found for |- Rel ( F ( D UP E ) W ) with typecode |-