# 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}}\left({A},{B}\right)↔{H}{Isom}_{{{R}}^{-1},{{S}}^{-1}}\left({A},{B}\right)$

### Proof

Step Hyp Ref Expression
1 ralcom ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}↔{H}\left({y}\right){S}{H}\left({x}\right)\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}↔{H}\left({y}\right){S}{H}\left({x}\right)\right)$
2 vex ${⊢}{x}\in \mathrm{V}$
3 vex ${⊢}{y}\in \mathrm{V}$
4 2 3 brcnv ${⊢}{x}{{R}}^{-1}{y}↔{y}{R}{x}$
5 fvex ${⊢}{H}\left({x}\right)\in \mathrm{V}$
6 fvex ${⊢}{H}\left({y}\right)\in \mathrm{V}$
7 5 6 brcnv ${⊢}{H}\left({x}\right){{S}}^{-1}{H}\left({y}\right)↔{H}\left({y}\right){S}{H}\left({x}\right)$
8 4 7 bibi12i ${⊢}\left({x}{{R}}^{-1}{y}↔{H}\left({x}\right){{S}}^{-1}{H}\left({y}\right)\right)↔\left({y}{R}{x}↔{H}\left({y}\right){S}{H}\left({x}\right)\right)$
9 8 2ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{{R}}^{-1}{y}↔{H}\left({x}\right){{S}}^{-1}{H}\left({y}\right)\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}↔{H}\left({y}\right){S}{H}\left({x}\right)\right)$
10 1 9 bitr4i ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}↔{H}\left({y}\right){S}{H}\left({x}\right)\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{{R}}^{-1}{y}↔{H}\left({x}\right){{S}}^{-1}{H}\left({y}\right)\right)$
11 10 anbi2i ${⊢}\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}↔{H}\left({y}\right){S}{H}\left({x}\right)\right)\right)↔\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{{R}}^{-1}{y}↔{H}\left({x}\right){{S}}^{-1}{H}\left({y}\right)\right)\right)$
12 df-isom ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)↔\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}↔{H}\left({y}\right){S}{H}\left({x}\right)\right)\right)$
13 df-isom ${⊢}{H}{Isom}_{{{R}}^{-1},{{S}}^{-1}}\left({A},{B}\right)↔\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{{R}}^{-1}{y}↔{H}\left({x}\right){{S}}^{-1}{H}\left({y}\right)\right)\right)$
14 11 12 13 3bitr4i ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)↔{H}{Isom}_{{{R}}^{-1},{{S}}^{-1}}\left({A},{B}\right)$