Metamath Proof Explorer

Theorem isoeq1

Description: Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004)

Ref Expression
Assertion isoeq1 ${⊢}{H}={G}\to \left({H}{Isom}_{{R},{S}}\left({A},{B}\right)↔{G}{Isom}_{{R},{S}}\left({A},{B}\right)\right)$

Proof

Step Hyp Ref Expression
1 f1oeq1 ${⊢}{H}={G}\to \left({H}:{A}\underset{1-1 onto}{⟶}{B}↔{G}:{A}\underset{1-1 onto}{⟶}{B}\right)$
2 fveq1 ${⊢}{H}={G}\to {H}\left({x}\right)={G}\left({x}\right)$
3 fveq1 ${⊢}{H}={G}\to {H}\left({y}\right)={G}\left({y}\right)$
4 2 3 breq12d ${⊢}{H}={G}\to \left({H}\left({x}\right){S}{H}\left({y}\right)↔{G}\left({x}\right){S}{G}\left({y}\right)\right)$
5 4 bibi2d ${⊢}{H}={G}\to \left(\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)↔\left({x}{R}{y}↔{G}\left({x}\right){S}{G}\left({y}\right)\right)\right)$
6 5 2ralbidv ${⊢}{H}={G}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{G}\left({x}\right){S}{G}\left({y}\right)\right)\right)$
7 1 6 anbi12d ${⊢}{H}={G}\to \left(\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}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)\right)↔\left({G}:{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}{y}↔{G}\left({x}\right){S}{G}\left({y}\right)\right)\right)\right)$
8 df-isom ${⊢}{H}{Isom}_{{R},{S}}\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}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)\right)$
9 df-isom ${⊢}{G}{Isom}_{{R},{S}}\left({A},{B}\right)↔\left({G}:{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}{y}↔{G}\left({x}\right){S}{G}\left({y}\right)\right)\right)$
10 7 8 9 3bitr4g ${⊢}{H}={G}\to \left({H}{Isom}_{{R},{S}}\left({A},{B}\right)↔{G}{Isom}_{{R},{S}}\left({A},{B}\right)\right)$