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

Definition df-isom 5447
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 5439 . 2
71, 2, 5wf1o 5437 . . 3
8 vx . . . . . . . 8
98cv 1669 . . . . . . 7
10 vy . . . . . . . 8
1110cv 1669 . . . . . . 7
129, 11, 3wbr 4318 . . . . . 6
139, 5cfv 5438 . . . . . . 7
1411, 5cfv 5438 . . . . . . 7
1513, 14, 4wbr 4318 . . . . . 6
1612, 15wb 178 . . . . 5
1716, 10, 1wral 2759 . . . 4
1817, 8, 1wral 2759 . . 3
197, 18wa 360 . 2
206, 19wb 178 1
Colors of variables: wff set class
This definition is referenced by:  isoeq1  6020  isoeq2  6021  isoeq3  6022  isoeq4  6023  isoeq5  6024  nfiso  6025  isof1o  6026  isorel  6027  soisores  6028  soisoi  6029  isoid  6030  isocnv  6031  isocnv2  6032  isocnv3  6033  isores2  6034  isores3  6036  isotr  6037  isoini2  6040  f1oiso  6052  f1owe  6054  smoiso2  6793  alephiso  8150  compssiso  8425  negiso  10172  om2uzisoi  11626  icopnfhmeo  19983  reefiso  21379  logltb  21514  isoun  25127  xrmulc1cn  25539  wepwsolem  28542  iso0  28767
  Copyright terms: Public domain W3C validator