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

Definition df-isom 5426
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 5418 . 2
71, 2, 5wf1o 5416 . . 3
8 vx . . . . . . . 8
98cv 1661 . . . . . . 7
10 vy . . . . . . . 8
1110cv 1661 . . . . . . 7
129, 11, 3wbr 4302 . . . . . 6
139, 5cfv 5417 . . . . . . 7
1411, 5cfv 5417 . . . . . . 7
1513, 14, 4wbr 4302 . . . . . 6
1612, 15wb 178 . . . . 5
1716, 10, 1wral 2751 . . . 4
1817, 8, 1wral 2751 . . 3
197, 18wa 360 . 2
206, 19wb 178 1
Colors of variables: wff set class
This definition is referenced by:  isoeq1  5984  isoeq2  5985  isoeq3  5986  isoeq4  5987  isoeq5  5988  nfiso  5989  isof1o  5990  isorel  5991  soisores  5992  soisoi  5993  isoid  5994  isocnv  5995  isocnv2  5996  isocnv3  5997  isores2  5998  isores3  6000  isotr  6001  isoini2  6004  f1oiso  6016  f1owe  6018  smoiso2  6743  alephiso  8093  compssiso  8368  negiso  10115  om2uzisoi  11569  icopnfhmeo  19472  reefiso  20868  logltb  21003  isoun  24618  xrmulc1cn  25030  wepwsolem  28045  iso0  28442
  Copyright terms: Public domain W3C validator