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	⊢ ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cH	⊢ 𝐻
1		cR	⊢ 𝑅
2		cS	⊢ 𝑆
3		cA	⊢ 𝐴
4		cB	⊢ 𝐵
5	3 4 1 2 0	wrelp	⊢ 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 )
6	3 4 0	wf	⊢ 𝐻 : 𝐴 ⟶ 𝐵
7		vx	⊢ 𝑥
8		vy	⊢ 𝑦
9	7	cv	⊢ 𝑥
10	8	cv	⊢ 𝑦
11	9 10 1	wbr	⊢ 𝑥 𝑅 𝑦
12	9 0	cfv	⊢ ( 𝐻 ‘ 𝑥 )
13	10 0	cfv	⊢ ( 𝐻 ‘ 𝑦 )
14	12 13 2	wbr	⊢ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 )
15	11 14	wi	⊢ ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) )
16	15 8 3	wral	⊢ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) )
17	16 7 3	wral	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) )
18	6 17	wa	⊢ ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
19	5 18	wb	⊢ ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )