Metamath Proof Explorer


Theorem isorel

Description: An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004)

Ref Expression
Assertion isorel H Isom R , S A B C A D A C R D H C S H D

Proof

Step Hyp Ref Expression
1 df-isom H Isom R , S A B H : A 1-1 onto B x A y A x R y H x S H y
2 1 simprbi H Isom R , S A B x A y A x R y H x S H y
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 bibi12d 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 bibi12d 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 H Isom R , S A B C A D A C R D H C S H D