df-iso - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > df-iso		Unicode version

Definition df-iso 4796

Description: Define the isomorphism predicate. We read this as "

is an

isomorphism of

onto

." Normally,

and

are ordering relations on

and

respectively. Definition 6.28 of [TakeutiZaring] p. 32, whose notation is the same as ours except that

and

are subscripts. (Contributed by SF, 5-Jan-2015.)

**Assertion**
Ref	Expression
df-iso	$/\$

**Detailed syntax breakdown of Definition df-iso**
Step	Hyp	Ref	Expression
1		cA	. . 3
2		cB	. . 3
3		cR	. . 3
4		cS	. . 3
5		cH	. . 3
6	1, 2, 3, 4, 5	wiso 4782	. 2
7	1, 2, 5	wf1o 4780	. . 3
8		vx	. . . . . . . 8
9	8	cv 1641	. . . . . . 7
10		vy	. . . . . . . 8
11	10	cv 1641	. . . . . . 7
12	9, 11, 3	wbr 4639	. . . . . 6
13	9, 5	cfv 4781	. . . . . . 7
14	11, 5	cfv 4781	. . . . . . 7
15	13, 14, 4	wbr 4639	. . . . . 6
16	12, 15	wb 176	. . . . 5
17	16, 10, 1	wral 2614	. . . 4
18	17, 8, 1	wral 2614	. . 3
19	7, 18	wa 358	. 2 $/\$
20	6, 19	wb 176	1 $/\$

Colors of variables: wff setvar class

This definition is referenced by: isoeq1 5482 isoeq2 5483 isoeq3 5484 isoeq4 5485 isoeq5 5486 nfiso 5487 isof1o 5488 isorel 5489 isoid 5490 isocnv 5491 isocnv2 5492 isores2 5493 isotr 5495 isoini2 5498 f1oiso 5499