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 Could not format assertion : No typesetting found for |- ( 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 ) ) ) ) with typecode |-

Detailed syntax breakdown

Step Hyp Ref Expression
0 cH class H
1 cR class R
2 cS class S
3 cA class A
4 cB class B
5 3 4 1 2 0 wrelp Could not format H RelPres R , S ( A , B ) : No typesetting found for wff H RelPres R , S ( A , B ) with typecode wff
6 3 4 0 wf wff H : A B
7 vx setvar x
8 vy setvar y
9 7 cv setvar x
10 8 cv setvar y
11 9 10 1 wbr wff x R y
12 9 0 cfv class H x
13 10 0 cfv class H y
14 12 13 2 wbr wff H x S H y
15 11 14 wi wff x R y H x S H y
16 15 8 3 wral wff y A x R y H x S H y
17 16 7 3 wral wff x A y A x R y H x S H y
18 6 17 wa wff H : A B x A y A x R y H x S H y
19 5 18 wb Could not format ( 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 ) ) ) ) : No typesetting found for wff ( 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 ) ) ) ) with typecode wff