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 ) )