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	$$classH$$
1		cR	$$classR$$
2		cS	$$classS$$
3		cA	$$classA$$
4		cB	$$classB$$
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	$$wffH:A⟶B$$
7		vx	$$setvarx$$
8		vy	$$setvary$$
9	7	cv	$$setvarx$$
10	8	cv	$$setvary$$
11	9 10 1	wbr	$$wffxRy$$
12	9 0	cfv	$$classH\left(x\right)$$
13	10 0	cfv	$$classH\left(y\right)$$
14	12 13 2	wbr	$$wffH\left(x\right)SH\left(y\right)$$
15	11 14	wi	$$wff\left(xRy\to H\left(x\right)SH\left(y\right)\right)$$
16	15 8 3	wral	$$wff\forall y\in A\left(xRy\to H\left(x\right)SH\left(y\right)\right)$$
17	16 7 3	wral	$$wff\forall x\in A\forall y\in A\left(xRy\to H\left(x\right)SH\left(y\right)\right)$$
18	6 17	wa	$$wff\left(H:A⟶B\wedge \forall x\in A\forall y\in A\left(xRy\to H\left(x\right)SH\left(y\right)\right)\right)$$
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