Definition df-relp 44921

Description: Define the relation-preserving predicate. This is a viable notion of "homomorphism" corresponding to df-isom 6550. (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 44920	. 2 wff 𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵)
7	1, 2, 5	wf 6537	. . 3 wff 𝐻:𝐴⟶𝐵
8		vx	. . . . . . . 8 setvar 𝑥
9	8	cv 1538	. . . . . . 7 class 𝑥
10		vy	. . . . . . . 8 setvar 𝑦
11	10	cv 1538	. . . . . . 7 class 𝑦
12	9, 11, 3	wbr 5123	. . . . . 6 wff 𝑥𝑅𝑦
13	9, 5	cfv 6541	. . . . . . 7 class (𝐻‘𝑥)
14	11, 5	cfv 6541	. . . . . . 7 class (𝐻‘𝑦)
15	13, 14, 4	wbr 5123	. . . . . 6 wff (𝐻‘𝑥)𝑆(𝐻‘𝑦)
16	12, 15	wi 4	. . . . 5 wff (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))
17	16, 10, 1	wral 3050	. . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))
18	17, 8, 1	wral 3050	. . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))
19	7, 18	wa 395	. 2 wff (𝐻:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
20	6, 19	wb 206	1 wff (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ (𝐻:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))))

This definition is referenced by:  relpeq1  44922  relpeq2  44923  relpeq3  44924  relpeq4  44925  relpeq5  44926  nfrelp  44927  relpf  44928  relprel  44929  rankrelp  44934