Step |
Hyp |
Ref |
Expression |
1 |
|
df-isom |
|- ( H Isom R , S ( A , B ) <-> ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) ) |
2 |
1
|
simprbi |
|- ( H Isom R , S ( A , B ) -> A. x e. A A. y e. 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 e. A /\ D e. A ) -> ( A. x e. A A. y e. 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 e. A /\ D e. A ) ) -> ( C R D <-> ( H ` C ) S ( H ` D ) ) ) |