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)\leftrightarrow \left(H:A\underset{1-1\; onto}{⟶}B\wedge \forall x\in A\forall y\in A\left(xRy\leftrightarrow H\left(x\right)SH\left(y\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cH	$$classH$$
1		cR	$$classR$$
2		cS	$$classS$$
3		cA	$$classA$$
4		cB	$$classB$$
5	3 4 1 2 0	wiso	$$wffH{Isom}_{R,S}\left(A,B\right)$$
6	3 4 0	wf1o	$$wffH:A\underset{1-1\; onto}{⟶}B$$
7		vx	$$setvarx$$
8		vy	$$setvary$$
9	7	cv	$$setvarx$$
10	8	cv	$$setvary$$
11	9 10 1	wbr	$$wffxRy$$
12	9 0	cfv	$$classH\left(x\right)$$
13	10 0	cfv	$$classH\left(y\right)$$
14	12 13 2	wbr	$$wffH\left(x\right)SH\left(y\right)$$
15	11 14	wb	$$wff\left(xRy\leftrightarrow H\left(x\right)SH\left(y\right)\right)$$
16	15 8 3	wral	$$wff\forall y\in A\left(xRy\leftrightarrow H\left(x\right)SH\left(y\right)\right)$$
17	16 7 3	wral	$$wff\forall x\in A\forall y\in A\left(xRy\leftrightarrow H\left(x\right)SH\left(y\right)\right)$$
18	6 17	wa	$$wff\left(H:A\underset{1-1\; onto}{⟶}B\wedge \forall x\in A\forall y\in A\left(xRy\leftrightarrow H\left(x\right)SH\left(y\right)\right)\right)$$
19	5 18	wb	$$wff\left(H{Isom}_{R,S}\left(A,B\right)\leftrightarrow \left(H:A\underset{1-1\; onto}{⟶}B\wedge \forall x\in A\forall y\in A\left(xRy\leftrightarrow H\left(x\right)SH\left(y\right)\right)\right)\right)$$