Metamath Proof Explorer

Theorem reldmup2

Description: The domain of ( D UP E ) is a relation. (Contributed by Zhi Wang, 16-Oct-2025)

Ref Expression
Assertion reldmup2 
|- Rel dom ( D UP E )

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 
 |-  ( 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 ) ) } )
7 6 reldmmpo 
 |-  Rel dom ( D UP E )