MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-isom Unicode version

Definition df-isom 5602
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 NM, 4-Mar-1997.)
Assertion
Ref Expression
df-isom
Distinct variable groups:   , ,   , ,   , ,   ,S,   , ,

Detailed syntax breakdown of Definition df-isom
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cR . . 3
4 cS . . 3
5 cH . . 3
61, 2, 3, 4, 5wiso 5594 . 2
71, 2, 5wf1o 5592 . . 3
8 vx . . . . . . . 8
98cv 1394 . . . . . . 7
10 vy . . . . . . . 8
1110cv 1394 . . . . . . 7
129, 11, 3wbr 4452 . . . . . 6
139, 5cfv 5593 . . . . . . 7
1411, 5cfv 5593 . . . . . . 7
1513, 14, 4wbr 4452 . . . . . 6
1612, 15wb 184 . . . . 5
1716, 10, 1wral 2807 . . . 4
1817, 8, 1wral 2807 . . 3
197, 18wa 369 . 2
206, 19wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  isoeq1  6215  isoeq2  6216  isoeq3  6217  isoeq4  6218  isoeq5  6219  nfiso  6220  isof1o  6221  isorel  6222  soisores  6223  soisoi  6224  isoid  6225  isocnv  6226  isocnv2  6227  isocnv3  6228  isores2  6229  isores3  6231  isotr  6232  isoini2  6235  f1oiso  6247  f1owe  6249  smoiso2  7059  alephiso  8500  compssiso  8775  negiso  10544  om2uzisoi  12065  icopnfhmeo  21443  reefiso  22843  logltb  22984  isoun  27520  xrmulc1cn  27912  wepwsolem  30987  iso0  31187  fourierdlem54  31943
  Copyright terms: Public domain W3C validator