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 6226
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 6218 . 2 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
71, 2, 5wf1o 6216 . . 3 wff 𝐻:𝐴1-1-onto𝐵
8 vx . . . . . . . 8 setvar 𝑥
98cv 1519 . . . . . . 7 class 𝑥
10 vy . . . . . . . 8 setvar 𝑦
1110cv 1519 . . . . . . 7 class 𝑦
129, 11, 3wbr 4956 . . . . . 6 wff 𝑥𝑅𝑦
139, 5cfv 6217 . . . . . . 7 class (𝐻𝑥)
1411, 5cfv 6217 . . . . . . 7 class (𝐻𝑦)
1513, 14, 4wbr 4956 . . . . . 6 wff (𝐻𝑥)𝑆(𝐻𝑦)
1612, 15wb 207 . . . . 5 wff (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))
1716, 10, 1wral 3103 . . . 4 wff 𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))
1817, 8, 1wral 3103 . . 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  6924  isoeq2  6925  isoeq3  6926  isoeq4  6927  isoeq5  6928  nfiso  6929  isof1o  6930  isof1oidb  6931  isof1oopb  6932  isorel  6933  soisores  6934  soisoi  6935  isoid  6936  isocnv  6937  isocnv2  6938  isocnv3  6939  isores2  6940  isores3  6942  isotr  6943  isoini2  6946  f1oiso  6958  f1owe  6960  smoiso2  7849  alephiso  9359  compssiso  9631  negiso  11458  om2uzisoi  13160  icopnfhmeo  23218  reefiso  24707  logltb  24852  isoun  30098  xrmulc1cn  30746  wepwsolem  39078  alephiso2  39353  iso0  40129  fourierdlem54  41941  rrx2plordisom  44145
  Copyright terms: Public domain W3C validator