Metamath Proof Explorer


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 x R y C R y
4 fveq2 x = C H x = H C
5 4 breq1d x = C H x S H y H C S H y
6 3 5 imbi12d x = C x R y H x S H y C R y H C S H y
7 breq2 y = D C R y C R D
8 fveq2 y = D H y = H D
9 8 breq2d y = D H C S H y H C S H D
10 7 9 imbi12d y = D C R y H C S H y C R D H C S H D
11 6 10 rspc2v C A D A x A y A x R y H x S H y C R D H C S H D
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 |-