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

Definition df-isom 6358
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 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝑅,𝑦   𝑥,𝑆,𝑦   𝑥,𝐻,𝑦

Detailed syntax breakdown of Definition df-isom
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cR . . 3 class 𝑅
4 cS . . 3 class 𝑆
5 cH . . 3 class 𝐻
61, 2, 3, 4, 5wiso 6350 . 2 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
71, 2, 5wf1o 6348 . . 3 wff 𝐻:𝐴1-1-onto𝐵
8 vx . . . . . . . 8 setvar 𝑥
98cv 1527 . . . . . . 7 class 𝑥
10 vy . . . . . . . 8 setvar 𝑦
1110cv 1527 . . . . . . 7 class 𝑦
129, 11, 3wbr 5058 . . . . . 6 wff 𝑥𝑅𝑦
139, 5cfv 6349 . . . . . . 7 class (𝐻𝑥)
1411, 5cfv 6349 . . . . . . 7 class (𝐻𝑦)
1513, 14, 4wbr 5058 . . . . . 6 wff (𝐻𝑥)𝑆(𝐻𝑦)
1612, 15wb 207 . . . . 5 wff (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))
1716, 10, 1wral 3138 . . . 4 wff 𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))
1817, 8, 1wral 3138 . . 3 wff 𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))
197, 18wa 396 . 2 wff (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)))
206, 19wb 207 1 wff (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
Colors of variables: wff setvar class
This definition is referenced by:  isoeq1  7059  isoeq2  7060  isoeq3  7061  isoeq4  7062  isoeq5  7063  nfiso  7064  isof1o  7065  isof1oidb  7066  isof1oopb  7067  isorel  7068  soisores  7069  soisoi  7070  isoid  7071  isocnv  7072  isocnv2  7073  isocnv3  7074  isores2  7075  isores3  7077  isotr  7078  isoini2  7081  f1oiso  7093  f1owe  7095  smoiso2  7997  alephiso  9513  compssiso  9785  negiso  11610  om2uzisoi  13312  icopnfhmeo  23476  reefiso  24965  logltb  25110  isoun  30364  xrmulc1cn  31073  wepwsolem  39522  alephiso2  39797  iso0  40519  fourierdlem54  42326  rrx2plordisom  44608
  Copyright terms: Public domain W3C validator