This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isocnv2

Description: Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014)

Ref Expression
Assertion isocnv2 
|- ( H Isom R , S ( A , B ) <-> H Isom `' R , `' S ( A , B ) )

Proof

Step Hyp Ref Expression
1 ralcom 
 |-  ( A. y e. A A. x e. A ( y R x <-> ( H ` y ) S ( H ` x ) ) <-> A. x e. A A. y e. A ( y R x <-> ( H ` y ) S ( H ` x ) ) )
2 vex 
 |-  x e. _V
3 vex 
 |-  y e. _V
4 2 3 brcnv 
 |-  ( x `' R y <-> y R x )
5 fvex 
 |-  ( H ` x ) e. _V
6 fvex 
 |-  ( H ` y ) e. _V
7 5 6 brcnv 
 |-  ( ( H ` x ) `' S ( H ` y ) <-> ( H ` y ) S ( H ` x ) )
8 4 7 bibi12i 
 |-  ( ( x `' R y <-> ( H ` x ) `' S ( H ` y ) ) <-> ( y R x <-> ( H ` y ) S ( H ` x ) ) )
9 8 2ralbii 
 |-  ( A. x e. A A. y e. A ( x `' R y <-> ( H ` x ) `' S ( H ` y ) ) <-> A. x e. A A. y e. A ( y R x <-> ( H ` y ) S ( H ` x ) ) )
10 1 9 bitr4i 
 |-  ( A. y e. A A. x e. A ( y R x <-> ( H ` y ) S ( H ` x ) ) <-> A. x e. A A. y e. A ( x `' R y <-> ( H ` x ) `' S ( H ` y ) ) )
11 10 anbi2i 
 |-  ( ( H : A -1-1-onto-> B /\ A. y e. A A. x e. A ( y R x <-> ( H ` y ) S ( H ` x ) ) ) <-> ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x `' R y <-> ( H ` x ) `' S ( H ` y ) ) ) )
12 df-isom 
 |-  ( H Isom R , S ( A , B ) <-> ( H : A -1-1-onto-> B /\ A. y e. A A. x e. A ( y R x <-> ( H ` y ) S ( H ` x ) ) ) )
13 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 ) ) ) )
14 11 12 13 3bitr4i 
 |-  ( H Isom R , S ( A , B ) <-> H Isom `' R , `' S ( A , B ) )