![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-isom | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-isom | ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | cR | . . 3 class 𝑅 | |
4 | cS | . . 3 class 𝑆 | |
5 | cH | . . 3 class 𝐻 | |
6 | 1, 2, 3, 4, 5 | wiso 6543 | . 2 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) |
7 | 1, 2, 5 | wf1o 6541 | . . 3 wff 𝐻:𝐴–1-1-onto→𝐵 |
8 | vx | . . . . . . . 8 setvar 𝑥 | |
9 | 8 | cv 1533 | . . . . . . 7 class 𝑥 |
10 | vy | . . . . . . . 8 setvar 𝑦 | |
11 | 10 | cv 1533 | . . . . . . 7 class 𝑦 |
12 | 9, 11, 3 | wbr 5142 | . . . . . 6 wff 𝑥𝑅𝑦 |
13 | 9, 5 | cfv 6542 | . . . . . . 7 class (𝐻‘𝑥) |
14 | 11, 5 | cfv 6542 | . . . . . . 7 class (𝐻‘𝑦) |
15 | 13, 14, 4 | wbr 5142 | . . . . . 6 wff (𝐻‘𝑥)𝑆(𝐻‘𝑦) |
16 | 12, 15 | wb 205 | . . . . 5 wff (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) |
17 | 16, 10, 1 | wral 3056 | . . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) |
18 | 17, 8, 1 | wral 3056 | . . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) |
19 | 7, 18 | wa 395 | . 2 wff (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) |
20 | 6, 19 | wb 205 | 1 wff (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) |
Colors of variables: wff setvar class |
This definition is referenced by: isoeq1 7319 isoeq2 7320 isoeq3 7321 isoeq4 7322 isoeq5 7323 nfiso 7324 isof1o 7325 isof1oidb 7326 isof1oopb 7327 isorel 7328 soisores 7329 soisoi 7330 isoid 7331 isocnv 7332 isocnv2 7333 isocnv3 7334 isores2 7335 isores3 7337 isotr 7338 isoini2 7341 f1oiso 7353 f1owe 7355 smoiso2 8383 alephiso 10113 compssiso 10389 negiso 12216 om2uzisoi 13943 icopnfhmeo 24855 reefiso 26372 logltb 26521 om2noseqiso 28162 isoun 32465 mgcf1o 32712 xrmulc1cn 33467 sticksstones3 41552 wepwsolem 42388 alephiso2 42911 iso0 43667 fourierdlem54 45471 rrx2plordisom 47719 |
Copyright terms: Public domain | W3C validator |