# Metamath Proof Explorer

## Theorem isof1oidb

Description: A function is a bijection iff it is an isomorphism regarding the identity relation. (Contributed by AV, 9-May-2021)

Ref Expression
Assertion isof1oidb ${⊢}{H}:{A}\underset{1-1 onto}{⟶}{B}↔{H}{Isom}_{\mathrm{I},\mathrm{I}}\left({A},{B}\right)$

### Proof

Step Hyp Ref Expression
1 f1of1 ${⊢}{H}:{A}\underset{1-1 onto}{⟶}{B}\to {H}:{A}\underset{1-1}{⟶}{B}$
2 f1fveq ${⊢}\left({H}:{A}\underset{1-1}{⟶}{B}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left({H}\left({x}\right)={H}\left({y}\right)↔{x}={y}\right)$
3 1 2 sylan ${⊢}\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left({H}\left({x}\right)={H}\left({y}\right)↔{x}={y}\right)$
4 fvex ${⊢}{H}\left({y}\right)\in \mathrm{V}$
5 4 ideq ${⊢}{H}\left({x}\right)\mathrm{I}{H}\left({y}\right)↔{H}\left({x}\right)={H}\left({y}\right)$
6 5 a1i ${⊢}\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left({H}\left({x}\right)\mathrm{I}{H}\left({y}\right)↔{H}\left({x}\right)={H}\left({y}\right)\right)$
7 ideqg ${⊢}{y}\in {A}\to \left({x}\mathrm{I}{y}↔{x}={y}\right)$
8 7 ad2antll ${⊢}\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left({x}\mathrm{I}{y}↔{x}={y}\right)$
9 3 6 8 3bitr4rd ${⊢}\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left({x}\mathrm{I}{y}↔{H}\left({x}\right)\mathrm{I}{H}\left({y}\right)\right)$
10 9 ralrimivva ${⊢}{H}:{A}\underset{1-1 onto}{⟶}{B}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{I}{y}↔{H}\left({x}\right)\mathrm{I}{H}\left({y}\right)\right)$
11 10 pm4.71i ${⊢}{H}:{A}\underset{1-1 onto}{⟶}{B}↔\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}\mathrm{I}{y}↔{H}\left({x}\right)\mathrm{I}{H}\left({y}\right)\right)\right)$
12 df-isom ${⊢}{H}{Isom}_{\mathrm{I},\mathrm{I}}\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}\mathrm{I}{y}↔{H}\left({x}\right)\mathrm{I}{H}\left({y}\right)\right)\right)$
13 11 12 bitr4i ${⊢}{H}:{A}\underset{1-1 onto}{⟶}{B}↔{H}{Isom}_{\mathrm{I},\mathrm{I}}\left({A},{B}\right)$