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 6571
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 6563 . 2 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
71, 2, 5wf1o 6561 . . 3 wff 𝐻:𝐴1-1-onto𝐵
8 vx . . . . . . . 8 setvar 𝑥
98cv 1535 . . . . . . 7 class 𝑥
10 vy . . . . . . . 8 setvar 𝑦
1110cv 1535 . . . . . . 7 class 𝑦
129, 11, 3wbr 5147 . . . . . 6 wff 𝑥𝑅𝑦
139, 5cfv 6562 . . . . . . 7 class (𝐻𝑥)
1411, 5cfv 6562 . . . . . . 7 class (𝐻𝑦)
1513, 14, 4wbr 5147 . . . . . 6 wff (𝐻𝑥)𝑆(𝐻𝑦)
1612, 15wb 206 . . . . 5 wff (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))
1716, 10, 1wral 3058 . . . 4 wff 𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))
1817, 8, 1wral 3058 . . 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  7336  isoeq2  7337  isoeq3  7338  isoeq4  7339  isoeq5  7340  nfiso  7341  isof1o  7342  isof1oidb  7343  isof1oopb  7344  isorel  7345  soisores  7346  soisoi  7347  isoid  7348  isocnv  7349  isocnv2  7350  isocnv3  7351  isores2  7352  isores3  7354  isotr  7355  isoini2  7358  f1oiso  7370  f1owe  7372  smoiso2  8407  alephiso  10135  compssiso  10411  negiso  12245  om2uzisoi  13991  icopnfhmeo  24987  reefiso  26506  logltb  26656  om2noseqiso  28322  isoun  32716  mgcf1o  32977  xrmulc1cn  33890  sticksstones3  42129  wepwsolem  43030  alephiso2  43547  iso0  44302  fourierdlem54  46115  rrx2plordisom  48572
  Copyright terms: Public domain W3C validator