Definition df-relp 45885

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

Assertion

Ref	Expression
df-relp	⊢ (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ (𝐻:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝑅,𝑦   𝑥,𝑆,𝑦   𝑥,𝐻,𝑦

Detailed syntax breakdown of Definition df-relp

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cR	. . 3 class 𝑅
4		cS	. . 3 class 𝑆
5		cH	. . 3 class 𝐻
6	1, 2, 3, 4, 5	wrelp 45884	. 2 wff 𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵)
7	1, 2, 5	wf 6527	. . 3 wff 𝐻:𝐴⟶𝐵
8		vx	. . . . . . . 8 setvar 𝑥
9	8	cv 1569	. . . . . . 7 class 𝑥
10		vy	. . . . . . . 8 setvar 𝑦
11	10	cv 1569	. . . . . . 7 class 𝑦
12	9, 11, 3	wbr 5103	. . . . . 6 wff 𝑥𝑅𝑦
13	9, 5	cfv 6531	. . . . . . 7 class (𝐻‘𝑥)
14	11, 5	cfv 6531	. . . . . . 7 class (𝐻‘𝑦)
15	13, 14, 4	wbr 5103	. . . . . 6 wff (𝐻‘𝑥)𝑆(𝐻‘𝑦)
16	12, 15	wi 4	. . . . 5 wff (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))
17	16, 10, 1	wral 3077	. . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))
18	17, 8, 1	wral 3077	. . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))
19	7, 18	wa 401	. 2 wff (𝐻:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
20	6, 19	wb 209	1 wff (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ (𝐻:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))))

This definition is used by:  relpeq1  45886  relpeq2  45887  relpeq3  45888  relpeq4  45889  relpeq5  45890  nfrelp  45891  relpf  45892  relprel  45893  rankrelp  45902