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 -1 Isom S , R B A

Proof

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