# Metamath Proof Explorer

## Definition df-isom

Description: Define the isomorphism predicate. We read this as " H is an R , S isomorphism of A onto B ". Normally, R and S are ordering relations on A and B respectively. Definition 6.28 of TakeutiZaring p. 32, whose notation is the same as ours except that R and S are subscripts. (Contributed by NM, 4-Mar-1997)

Ref Expression
Assertion 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)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cH ${class}{H}$
1 cR ${class}{R}$
2 cS ${class}{S}$
3 cA ${class}{A}$
4 cB ${class}{B}$
5 3 4 1 2 0 wiso ${wff}{H}{Isom}_{{R},{S}}\left({A},{B}\right)$
6 3 4 0 wf1o ${wff}{H}:{A}\underset{1-1 onto}{⟶}{B}$
7 vx ${setvar}{x}$
8 vy ${setvar}{y}$
9 7 cv ${setvar}{x}$
10 8 cv ${setvar}{y}$
11 9 10 1 wbr ${wff}{x}{R}{y}$
12 9 0 cfv ${class}{H}\left({x}\right)$
13 10 0 cfv ${class}{H}\left({y}\right)$
14 12 13 2 wbr ${wff}{H}\left({x}\right){S}{H}\left({y}\right)$
15 11 14 wb ${wff}\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)$
16 15 8 3 wral ${wff}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}↔{H}\left({x}\right){S}{H}\left({y}\right)\right)$
17 16 7 3 wral ${wff}\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)$
18 6 17 wa ${wff}\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)$
19 5 18 wb ${wff}\left({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)\right)$