Metamath Proof Explorer

Definition df-relp

Description: Define the relation-preserving predicate. This is a viable notion of "homomorphism" corresponding to df-isom . (Contributed by Eric Schmidt, 11-Oct-2025)

Ref Expression
Assertion df-relp 
|- ( H RelPres R , S ( A , B ) <-> ( H : A --> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cH 
 |-  H
1 cR 
 |-  R
2 cS 
 |-  S
3 cA 
 |-  A
4 cB 
 |-  B
5 3 4 1 2 0 wrelp 
 |-  H RelPres R , S ( A , B )
6 3 4 0 wf 
 |-  H : A --> B
7 vx 
 |-  x
8 vy 
 |-  y
9 7 cv 
 |-  x
10 8 cv 
 |-  y
11 9 10 1 wbr 
 |-  x R y
12 9 0 cfv 
 |-  ( H ` x )
13 10 0 cfv 
 |-  ( H ` y )
14 12 13 2 wbr 
 |-  ( H ` x ) S ( H ` y )
15 11 14 wi 
 |-  ( x R y -> ( H ` x ) S ( H ` y ) )
16 15 8 3 wral 
 |-  A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) )
17 16 7 3 wral 
 |-  A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) )
18 6 17 wa 
 |-  ( H : A --> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) )
19 5 18 wb 
 |-  ( H RelPres R , S ( A , B ) <-> ( H : A --> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) )