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 6117
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 6109 . 2 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
71, 2, 5wf1o 6107 . . 3 wff 𝐻:𝐴1-1-onto𝐵
8 vx . . . . . . . 8 setvar 𝑥
98cv 1636 . . . . . . 7 class 𝑥
10 vy . . . . . . . 8 setvar 𝑦
1110cv 1636 . . . . . . 7 class 𝑦
129, 11, 3wbr 4855 . . . . . 6 wff 𝑥𝑅𝑦
139, 5cfv 6108 . . . . . . 7 class (𝐻𝑥)
1411, 5cfv 6108 . . . . . . 7 class (𝐻𝑦)
1513, 14, 4wbr 4855 . . . . . 6 wff (𝐻𝑥)𝑆(𝐻𝑦)
1612, 15wb 197 . . . . 5 wff (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))
1716, 10, 1wral 3107 . . . 4 wff 𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))
1817, 8, 1wral 3107 . . 3 wff 𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))
197, 18wa 384 . 2 wff (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)))
206, 19wb 197 1 wff (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
Colors of variables: wff setvar class
This definition is referenced by:  isoeq1  6798  isoeq2  6799  isoeq3  6800  isoeq4  6801  isoeq5  6802  nfiso  6803  isof1o  6804  isof1oidb  6805  isof1oopb  6806  isorel  6807  soisores  6808  soisoi  6809  isoid  6810  isocnv  6811  isocnv2  6812  isocnv3  6813  isores2  6814  isores3  6816  isotr  6817  isoini2  6820  f1oiso  6832  f1owe  6834  smoiso2  7709  alephiso  9211  compssiso  9488  negiso  11295  om2uzisoi  12984  icopnfhmeo  22963  reefiso  24426  logltb  24570  isoun  29816  xrmulc1cn  30311  wepwsolem  38118  iso0  39011  fourierdlem54  40861
  Copyright terms: Public domain W3C validator