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

Definition df-isom 5510
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 5502 . 2
71, 2, 5wf1o 5500 . . 3
8 vx . . . . . . . 8
98cv 1653 . . . . . . 7
10 vy . . . . . . . 8
1110cv 1653 . . . . . . 7
129, 11, 3wbr 4243 . . . . . 6
139, 5cfv 5501 . . . . . . 7
1411, 5cfv 5501 . . . . . . 7
1513, 14, 4wbr 4243 . . . . . 6
1612, 15wb 178 . . . . 5
1716, 10, 1wral 2712 . . . 4
1817, 8, 1wral 2712 . . 3
197, 18wa 360 . 2
206, 19wb 178 1
Colors of variables: wff set class
This definition is referenced by:  isoeq1  6087  isoeq2  6088  isoeq3  6089  isoeq4  6090  isoeq5  6091  nfiso  6092  isof1o  6093  isorel  6094  soisores  6095  soisoi  6096  isoid  6097  isocnv  6098  isocnv2  6099  isocnv3  6100  isores2  6101  isores3  6103  isotr  6104  isoini2  6107  f1oiso  6119  f1owe  6121  smoiso2  6680  alephiso  8030  compssiso  8305  negiso  10035  om2uzisoi  11345  icopnfhmeo  19019  reefiso  20415  logltb  20545  isoun  24137  xrmulc1cn  24365  wepwsolem  27295  iso0  27692
  Copyright terms: Public domain W3C validator