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 ⊢HIsomR,SAB→H-1IsomS,RBA

Proof

Step Hyp Ref Expression
1 f1ocnv ⊢H:A⟶1-1 ontoB→H-1:B⟶1-1 ontoA
2 1 adantr ⊢H:A⟶1-1 ontoB∧∀x∈A∀y∈AxRy↔H⁡xSH⁡y→H-1:B⟶1-1 ontoA
3 f1ocnvfv2 ⊢H:A⟶1-1 ontoB∧z∈B→H⁡H-1⁡z=z
4 3 adantrr ⊢H:A⟶1-1 ontoB∧z∈B∧w∈B→H⁡H-1⁡z=z
5 f1ocnvfv2 ⊢H:A⟶1-1 ontoB∧w∈B→H⁡H-1⁡w=w
6 5 adantrl ⊢H:A⟶1-1 ontoB∧z∈B∧w∈B→H⁡H-1⁡w=w
7 4 6 breq12d ⊢H:A⟶1-1 ontoB∧z∈B∧w∈B→H⁡H-1⁡zSH⁡H-1⁡w↔zSw
8 7 adantlr ⊢H:A⟶1-1 ontoB∧∀x∈A∀y∈AxRy↔H⁡xSH⁡y∧z∈B∧w∈B→H⁡H-1⁡zSH⁡H-1⁡w↔zSw
9 f1of ⊢H-1:B⟶1-1 ontoA→H-1:B⟶A
10 1 9 syl ⊢H:A⟶1-1 ontoB→H-1:B⟶A
11 ffvelcdm ⊢H-1:B⟶A∧z∈B→H-1⁡z∈A
12 ffvelcdm ⊢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→xRy↔H-1⁡zRy
15 fveq2 ⊢x=H-1⁡z→H⁡x=H⁡H-1⁡z
16 15 breq1d ⊢x=H-1⁡z→H⁡xSH⁡y↔H⁡H-1⁡zSH⁡y
17 14 16 bibi12d ⊢x=H-1⁡z→xRy↔H⁡xSH⁡y↔H-1⁡zRy↔H⁡H-1⁡zSH⁡y
18 bicom ⊢H-1⁡zRy↔H⁡H-1⁡zSH⁡y↔H⁡H-1⁡zSH⁡y↔H-1⁡zRy
19 17 18 bitrdi ⊢x=H-1⁡z→xRy↔H⁡xSH⁡y↔H⁡H-1⁡zSH⁡y↔H-1⁡zRy
20 fveq2 ⊢y=H-1⁡w→H⁡y=H⁡H-1⁡w
21 20 breq2d ⊢y=H-1⁡w→H⁡H-1⁡zSH⁡y↔H⁡H-1⁡zSH⁡H-1⁡w
22 breq2 ⊢y=H-1⁡w→H-1⁡zRy↔H-1⁡zRH-1⁡w
23 21 22 bibi12d ⊢y=H-1⁡w→H⁡H-1⁡zSH⁡y↔H-1⁡zRy↔H⁡H-1⁡zSH⁡H-1⁡w↔H-1⁡zRH-1⁡w
24 19 23 rspc2va ⊢H-1⁡z∈A∧H-1⁡w∈A∧∀x∈A∀y∈AxRy↔H⁡xSH⁡y→H⁡H-1⁡zSH⁡H-1⁡w↔H-1⁡zRH-1⁡w
25 13 24 sylan ⊢H-1:B⟶A∧z∈B∧w∈B∧∀x∈A∀y∈AxRy↔H⁡xSH⁡y→H⁡H-1⁡zSH⁡H-1⁡w↔H-1⁡zRH-1⁡w
26 25 an32s ⊢H-1:B⟶A∧∀x∈A∀y∈AxRy↔H⁡xSH⁡y∧z∈B∧w∈B→H⁡H-1⁡zSH⁡H-1⁡w↔H-1⁡zRH-1⁡w
27 10 26 sylanl1 ⊢H:A⟶1-1 ontoB∧∀x∈A∀y∈AxRy↔H⁡xSH⁡y∧z∈B∧w∈B→H⁡H-1⁡zSH⁡H-1⁡w↔H-1⁡zRH-1⁡w
28 8 27 bitr3d ⊢H:A⟶1-1 ontoB∧∀x∈A∀y∈AxRy↔H⁡xSH⁡y∧z∈B∧w∈B→zSw↔H-1⁡zRH-1⁡w
29 28 ralrimivva ⊢H:A⟶1-1 ontoB∧∀x∈A∀y∈AxRy↔H⁡xSH⁡y→∀z∈B∀w∈BzSw↔H-1⁡zRH-1⁡w
30 2 29 jca ⊢H:A⟶1-1 ontoB∧∀x∈A∀y∈AxRy↔H⁡xSH⁡y→H-1:B⟶1-1 ontoA∧∀z∈B∀w∈BzSw↔H-1⁡zRH-1⁡w
31 df-isom ⊢HIsomR,SAB↔H:A⟶1-1 ontoB∧∀x∈A∀y∈AxRy↔H⁡xSH⁡y
32 df-isom ⊢H-1IsomS,RBA↔H-1:B⟶1-1 ontoA∧∀z∈B∀w∈BzSw↔H-1⁡zRH-1⁡w
33 30 31 32 3imtr4i ⊢HIsomR,SAB→H-1IsomS,RBA