| 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 6562 | . 2 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) |
| 7 | 1, 2, 5 | wf1o 6560 | . . 3 wff 𝐻:𝐴–1-1-onto→𝐵 |
| 8 | vx | . . . . . . . 8 setvar 𝑥 | |
| 9 | 8 | cv 1539 | . . . . . . 7 class 𝑥 |
| 10 | vy | . . . . . . . 8 setvar 𝑦 | |
| 11 | 10 | cv 1539 | . . . . . . 7 class 𝑦 |
| 12 | 9, 11, 3 | wbr 5143 | . . . . . 6 wff 𝑥𝑅𝑦 |
| 13 | 9, 5 | cfv 6561 | . . . . . . 7 class (𝐻‘𝑥) |
| 14 | 11, 5 | cfv 6561 | . . . . . . 7 class (𝐻‘𝑦) |
| 15 | 13, 14, 4 | wbr 5143 | . . . . . 6 wff (𝐻‘𝑥)𝑆(𝐻‘𝑦) |
| 16 | 12, 15 | wb 206 | . . . . 5 wff (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) |
| 17 | 16, 10, 1 | wral 3061 | . . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) |
| 18 | 17, 8, 1 | wral 3061 | . . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) |
| 19 | 7, 18 | wa 395 | . 2 wff (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) |
| 20 | 6, 19 | wb 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 |