Metamath Proof Explorer

Theorem isocnv

Description: Converse law for isomorphism. Proposition 6.30(2) of TakeutiZaring p. 33. (Contributed by NM, 27-Apr-2004)

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

Proof

Step Hyp Ref Expression
1 f1ocnv 
 |-  ( H : A -1-1-onto-> B -> `' H : B -1-1-onto-> A )
2 1 adantr 
 |-  ( ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) -> `' H : B -1-1-onto-> A )
3 f1ocnvfv2 
 |-  ( ( H : A -1-1-onto-> B /\ z e. B ) -> ( H ` ( `' H ` z ) ) = z )
4 3 adantrr 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. B /\ w e. B ) ) -> ( H ` ( `' H ` z ) ) = z )
5 f1ocnvfv2 
 |-  ( ( H : A -1-1-onto-> B /\ w e. B ) -> ( H ` ( `' H ` w ) ) = w )
6 5 adantrl 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. B /\ w e. B ) ) -> ( H ` ( `' H ` w ) ) = w )
7 4 6 breq12d 
 |-  ( ( H : A -1-1-onto-> B /\ ( z e. B /\ w e. B ) ) -> ( ( H ` ( `' H ` z ) ) S ( H ` ( `' H ` w ) ) <-> z S w ) )
8 7 adantlr 
 |-  ( ( ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) /\ ( z e. B /\ w e. B ) ) -> ( ( H ` ( `' H ` z ) ) S ( H ` ( `' H ` w ) ) <-> z S w ) )
9 f1of 
 |-  ( `' H : B -1-1-onto-> A -> `' H : B --> A )
10 1 9 syl 
 |-  ( H : A -1-1-onto-> B -> `' H : B --> A )
11 ffvelcdm 
 |-  ( ( `' H : B --> A /\ z e. B ) -> ( `' H ` z ) e. A )
12 ffvelcdm 
 |-  ( ( `' H : B --> A /\ w e. B ) -> ( `' H ` w ) e. A )
13 11 12 anim12dan 
 |-  ( ( `' H : B --> A /\ ( z e. B /\ w e. B ) ) -> ( ( `' H ` z ) e. A /\ ( `' H ` w ) e. A ) )
14 breq1 
 |-  ( x = ( `' H ` z ) -> ( x R y <-> ( `' H ` z ) R y ) )
15 fveq2 
 |-  ( x = ( `' H ` z ) -> ( H ` x ) = ( H ` ( `' H ` z ) ) )
16 15 breq1d 
 |-  ( x = ( `' H ` z ) -> ( ( H ` x ) S ( H ` y ) <-> ( H ` ( `' H ` z ) ) S ( H ` y ) ) )
17 14 16 bibi12d 
 |-  ( x = ( `' H ` z ) -> ( ( x R y <-> ( H ` x ) S ( H ` y ) ) <-> ( ( `' H ` z ) R y <-> ( H ` ( `' H ` z ) ) S ( H ` y ) ) ) )
18 bicom 
 |-  ( ( ( `' H ` z ) R y <-> ( H ` ( `' H ` z ) ) S ( H ` y ) ) <-> ( ( H ` ( `' H ` z ) ) S ( H ` y ) <-> ( `' H ` z ) R y ) )
19 17 18 bitrdi 
 |-  ( x = ( `' H ` z ) -> ( ( x R y <-> ( H ` x ) S ( H ` y ) ) <-> ( ( H ` ( `' H ` z ) ) S ( H ` y ) <-> ( `' H ` z ) R y ) ) )
20 fveq2 
 |-  ( y = ( `' H ` w ) -> ( H ` y ) = ( H ` ( `' H ` w ) ) )
21 20 breq2d 
 |-  ( y = ( `' H ` w ) -> ( ( H ` ( `' H ` z ) ) S ( H ` y ) <-> ( H ` ( `' H ` z ) ) S ( H ` ( `' H ` w ) ) ) )
22 breq2 
 |-  ( y = ( `' H ` w ) -> ( ( `' H ` z ) R y <-> ( `' H ` z ) R ( `' H ` w ) ) )
23 21 22 bibi12d 
 |-  ( y = ( `' H ` w ) -> ( ( ( H ` ( `' H ` z ) ) S ( H ` y ) <-> ( `' H ` z ) R y ) <-> ( ( H ` ( `' H ` z ) ) S ( H ` ( `' H ` w ) ) <-> ( `' H ` z ) R ( `' H ` w ) ) ) )
24 19 23 rspc2va 
 |-  ( ( ( ( `' H ` z ) e. A /\ ( `' H ` w ) e. A ) /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) -> ( ( H ` ( `' H ` z ) ) S ( H ` ( `' H ` w ) ) <-> ( `' H ` z ) R ( `' H ` w ) ) )
25 13 24 sylan 
 |-  ( ( ( `' H : B --> A /\ ( z e. B /\ w e. B ) ) /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) -> ( ( H ` ( `' H ` z ) ) S ( H ` ( `' H ` w ) ) <-> ( `' H ` z ) R ( `' H ` w ) ) )
26 25 an32s 
 |-  ( ( ( `' H : B --> A /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) /\ ( z e. B /\ w e. B ) ) -> ( ( H ` ( `' H ` z ) ) S ( H ` ( `' H ` w ) ) <-> ( `' H ` z ) R ( `' H ` w ) ) )
27 10 26 sylanl1 
 |-  ( ( ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) /\ ( z e. B /\ w e. B ) ) -> ( ( H ` ( `' H ` z ) ) S ( H ` ( `' H ` w ) ) <-> ( `' H ` z ) R ( `' H ` w ) ) )
28 8 27 bitr3d 
 |-  ( ( ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) /\ ( z e. B /\ w e. B ) ) -> ( z S w <-> ( `' H ` z ) R ( `' H ` w ) ) )
29 28 ralrimivva 
 |-  ( ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) -> A. z e. B A. w e. B ( z S w <-> ( `' H ` z ) R ( `' H ` w ) ) )
30 2 29 jca 
 |-  ( ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) -> ( `' H : B -1-1-onto-> A /\ A. z e. B A. w e. B ( z S w <-> ( `' H ` z ) R ( `' H ` w ) ) ) )
31 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 ) ) ) )
32 df-isom 
 |-  ( `' H Isom S , R ( B , A ) <-> ( `' H : B -1-1-onto-> A /\ A. z e. B A. w e. B ( z S w <-> ( `' H ` z ) R ( `' H ` w ) ) ) )
33 30 31 32 3imtr4i 
 |-  ( H Isom R , S ( A , B ) -> `' H Isom S , R ( B , A ) )