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 6570
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 6562 . 2 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
71, 2, 5wf1o 6560 . . 3 wff 𝐻:𝐴1-1-onto𝐵
8 vx . . . . . . . 8 setvar 𝑥
98cv 1539 . . . . . . 7 class 𝑥
10 vy . . . . . . . 8 setvar 𝑦
1110cv 1539 . . . . . . 7 class 𝑦
129, 11, 3wbr 5143 . . . . . 6 wff 𝑥𝑅𝑦
139, 5cfv 6561 . . . . . . 7 class (𝐻𝑥)
1411, 5cfv 6561 . . . . . . 7 class (𝐻𝑦)
1513, 14, 4wbr 5143 . . . . . 6 wff (𝐻𝑥)𝑆(𝐻𝑦)
1612, 15wb 206 . . . . 5 wff (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))
1716, 10, 1wral 3061 . . . 4 wff 𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))
1817, 8, 1wral 3061 . . 3 wff 𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))
197, 18wa 395 . 2 wff (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)))
206, 19wb 206 1 wff (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
Colors of variables: wff setvar class
This definition is referenced by:  isoeq1  7337  isoeq2  7338  isoeq3  7339  isoeq4  7340  isoeq5  7341  nfiso  7342  isof1o  7343  isof1oidb  7344  isof1oopb  7345  isorel  7346  soisores  7347  soisoi  7348  isoid  7349  isocnv  7350  isocnv2  7351  isocnv3  7352  isores2  7353  isores3  7355  isotr  7356  isoini2  7359  f1oiso  7371  f1owe  7373  smoiso2  8409  alephiso  10138  compssiso  10414  negiso  12248  om2uzisoi  13995  icopnfhmeo  24974  reefiso  26492  logltb  26642  om2noseqiso  28308  isoun  32711  mgcf1o  32993  xrmulc1cn  33929  sticksstones3  42149  wepwsolem  43054  alephiso2  43571  iso0  44326  fourierdlem54  46175  rrx2plordisom  48644
  Copyright terms: Public domain W3C validator