Step |
Hyp |
Ref |
Expression |
1 |
|
f1oeq2 |
|- ( A = C -> ( H : A -1-1-onto-> B <-> H : C -1-1-onto-> B ) ) |
2 |
|
raleq |
|- ( A = C -> ( A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) <-> A. y e. C ( x R y <-> ( H ` x ) S ( H ` y ) ) ) ) |
3 |
2
|
raleqbi1dv |
|- ( A = C -> ( A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) <-> A. x e. C A. y e. C ( x R y <-> ( H ` x ) S ( H ` y ) ) ) ) |
4 |
1 3
|
anbi12d |
|- ( A = C -> ( ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) <-> ( H : C -1-1-onto-> B /\ A. x e. C A. y e. C ( x R y <-> ( H ` x ) S ( H ` y ) ) ) ) ) |
5 |
|
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 ) ) ) ) |
6 |
|
df-isom |
|- ( H Isom R , S ( C , B ) <-> ( H : C -1-1-onto-> B /\ A. x e. C A. y e. C ( x R y <-> ( H ` x ) S ( H ` y ) ) ) ) |
7 |
4 5 6
|
3bitr4g |
|- ( A = C -> ( H Isom R , S ( A , B ) <-> H Isom R , S ( C , B ) ) ) |