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 5895
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 5887 . 2 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
71, 2, 5wf1o 5885 . . 3 wff 𝐻:𝐴1-1-onto𝐵
8 vx . . . . . . . 8 setvar 𝑥
98cv 1481 . . . . . . 7 class 𝑥
10 vy . . . . . . . 8 setvar 𝑦
1110cv 1481 . . . . . . 7 class 𝑦
129, 11, 3wbr 4651 . . . . . 6 wff 𝑥𝑅𝑦
139, 5cfv 5886 . . . . . . 7 class (𝐻𝑥)
1411, 5cfv 5886 . . . . . . 7 class (𝐻𝑦)
1513, 14, 4wbr 4651 . . . . . 6 wff (𝐻𝑥)𝑆(𝐻𝑦)
1612, 15wb 196 . . . . 5 wff (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))
1716, 10, 1wral 2911 . . . 4 wff 𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))
1817, 8, 1wral 2911 . . 3 wff 𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))
197, 18wa 384 . 2 wff (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)))
206, 19wb 196 1 wff (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
Colors of variables: wff setvar class
This definition is referenced by:  isoeq1  6564  isoeq2  6565  isoeq3  6566  isoeq4  6567  isoeq5  6568  nfiso  6569  isof1o  6570  isof1oidb  6571  isof1oopb  6572  isorel  6573  soisores  6574  soisoi  6575  isoid  6576  isocnv  6577  isocnv2  6578  isocnv3  6579  isores2  6580  isores3  6582  isotr  6583  isoini2  6586  f1oiso  6598  f1owe  6600  smoiso2  7463  alephiso  8918  compssiso  9193  negiso  11000  om2uzisoi  12748  icopnfhmeo  22736  reefiso  24196  logltb  24340  isoun  29464  xrmulc1cn  29961  wepwsolem  37438  iso0  38332  fourierdlem54  40146
  Copyright terms: Public domain W3C validator