Definition df-isom 5422

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.)

Assertion

Ref	Expression
df-isom	|- ( H Isom R , S ( A , B ) <-> ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) )

Distinct variable groups:   x, y, A   x, B, y   x, R, y   x, S, y   x, H, y

Detailed syntax breakdown of Definition df-isom

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cR	. . 3 class R
4		cS	. . 3 class S
5		cH	. . 3 class H
6	1, 2, 3, 4, 5	wiso 5414	. 2 wff H Isom R , S ( A , B )
7	1, 2, 5	wf1o 5412	. . 3 wff H : A -1-1-onto-> B
8		vx	. . . . . . . 8 set x
9	8	cv 1648	. . . . . . 7 class x
10		vy	. . . . . . . 8 set y
11	10	cv 1648	. . . . . . 7 class y
12	9, 11, 3	wbr 4172	. . . . . 6 wff x R y
13	9, 5	cfv 5413	. . . . . . 7 class ( H ` x )
14	11, 5	cfv 5413	. . . . . . 7 class ( H ` y )
15	13, 14, 4	wbr 4172	. . . . . 6 wff ( H ` x ) S ( H ` y )
16	12, 15	wb 177	. . . . 5 wff ( x R y <-> ( H ` x ) S ( H ` y ) )
17	16, 10, 1	wral 2666	. . . 4 wff A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
18	17, 8, 1	wral 2666	. . 3 wff A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) )
19	7, 18	wa 359	. 2 wff ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) )
20	6, 19	wb 177	1 wff ( H Isom R , S ( A , B ) <-> ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) )

This definition is referenced by:  isoeq1  5998  isoeq2  5999  isoeq3  6000  isoeq4  6001  isoeq5  6002  nfiso  6003  isof1o  6004  isorel  6005  soisores  6006  soisoi  6007  isoid  6008  isocnv  6009  isocnv2  6010  isocnv3  6011  isores2  6012  isores3  6014  isotr  6015  isoini2  6018  f1oiso  6030  f1owe  6032  smoiso2  6590  alephiso  7935  compssiso  8210  negiso  9940  om2uzisoi  11249  icopnfhmeo  18921  reefiso  20317  logltb  20447  isoun  24042  xrmulc1cn  24269  wepwsolem  27006  iso0  27404