Theorem relprel

Description: A relation-preserving function preserves the relation. (Contributed by Eric Schmidt, 11-Oct-2025)

	Ref	Expression
Assertion	relprel	Could not format assertion : No typesetting found for |- ( ( H RelPres R , S ( A , B ) /\ ( C e. A /\ D e. A ) ) -> ( C R D -> ( H ` C ) S ( H ` D ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-relp	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 |- ( 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 |-
2	1	simprbi	Could not format ( H RelPres R , S ( A , B ) -> A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) : No typesetting found for |- ( H RelPres R , S ( A , B ) -> A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) with typecode |-
3		breq1	$$⊢x=C\to \left(xRy\leftrightarrow CRy\right)$$
4		fveq2	$$⊢x=C\to H\left(x\right)=H\left(C\right)$$
5	4	breq1d	$$⊢x=C\to \left(H\left(x\right)SH\left(y\right)\leftrightarrow H\left(C\right)SH\left(y\right)\right)$$
6	3 5	imbi12d	$$⊢x=C\to \left(\left(xRy\to H\left(x\right)SH\left(y\right)\right)\leftrightarrow \left(CRy\to H\left(C\right)SH\left(y\right)\right)\right)$$
7		breq2	$$⊢y=D\to \left(CRy\leftrightarrow CRD\right)$$
8		fveq2	$$⊢y=D\to H\left(y\right)=H\left(D\right)$$
9	8	breq2d	$$⊢y=D\to \left(H\left(C\right)SH\left(y\right)\leftrightarrow H\left(C\right)SH\left(D\right)\right)$$
10	7 9	imbi12d	$$⊢y=D\to \left(\left(CRy\to H\left(C\right)SH\left(y\right)\right)\leftrightarrow \left(CRD\to H\left(C\right)SH\left(D\right)\right)\right)$$
11	6 10	rspc2v	$$⊢\left(C\in A\wedge D\in A\right)\to \left(\forall x\in A\forall y\in A\left(xRy\to H\left(x\right)SH\left(y\right)\right)\to \left(CRD\to H\left(C\right)SH\left(D\right)\right)\right)$$
12	2 11	mpan9	Could not format ( ( H RelPres R , S ( A , B ) /\ ( C e. A /\ D e. A ) ) -> ( C R D -> ( H ` C ) S ( H ` D ) ) ) : No typesetting found for |- ( ( H RelPres R , S ( A , B ) /\ ( C e. A /\ D e. A ) ) -> ( C R D -> ( H ` C ) S ( H ` D ) ) ) with typecode |-