ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-isom GIF version

Definition df-isom 5224
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 5216 . 2 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)
71, 2, 5wf1o 5214 . . 3 wff 𝐻:𝐴1-1-onto𝐵
8 vx . . . . . . . 8 setvar 𝑥
98cv 1352 . . . . . . 7 class 𝑥
10 vy . . . . . . . 8 setvar 𝑦
1110cv 1352 . . . . . . 7 class 𝑦
129, 11, 3wbr 4002 . . . . . 6 wff 𝑥𝑅𝑦
139, 5cfv 5215 . . . . . . 7 class (𝐻𝑥)
1411, 5cfv 5215 . . . . . . 7 class (𝐻𝑦)
1513, 14, 4wbr 4002 . . . . . 6 wff (𝐻𝑥)𝑆(𝐻𝑦)
1612, 15wb 105 . . . . 5 wff (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))
1716, 10, 1wral 2455 . . . 4 wff 𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))
1817, 8, 1wral 2455 . . 3 wff 𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))
197, 18wa 104 . 2 wff (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)))
206, 19wb 105 1 wff (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
Colors of variables: wff set class
This definition is referenced by:  isoeq1  5799  isoeq2  5800  isoeq3  5801  isoeq4  5802  isoeq5  5803  nfiso  5804  isof1o  5805  isorel  5806  isoid  5808  isocnv  5809  isocnv2  5810  isores2  5811  isores3  5813  isotr  5814  iso0  5815  isoini2  5817  f1oiso  5824  negiso  8908  frec2uzisod  10402  zfz1isolem1  10813  xrnegiso  11263  reefiso  14069  logltb  14166
  Copyright terms: Public domain W3C validator