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 5805 | . 2 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) |
7 | 1, 2, 5 | wf1o 5803 | . . 3 wff 𝐻:𝐴–1-1-onto→𝐵 |
8 | vx | . . . . . . . 8 setvar 𝑥 | |
9 | 8 | cv 1474 | . . . . . . 7 class 𝑥 |
10 | vy | . . . . . . . 8 setvar 𝑦 | |
11 | 10 | cv 1474 | . . . . . . 7 class 𝑦 |
12 | 9, 11, 3 | wbr 4583 | . . . . . 6 wff 𝑥𝑅𝑦 |
13 | 9, 5 | cfv 5804 | . . . . . . 7 class (𝐻‘𝑥) |
14 | 11, 5 | cfv 5804 | . . . . . . 7 class (𝐻‘𝑦) |
15 | 13, 14, 4 | wbr 4583 | . . . . . 6 wff (𝐻‘𝑥)𝑆(𝐻‘𝑦) |
16 | 12, 15 | wb 195 | . . . . 5 wff (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) |
17 | 16, 10, 1 | wral 2896 | . . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) |
18 | 17, 8, 1 | wral 2896 | . . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) |
19 | 7, 18 | wa 383 | . 2 wff (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) |
20 | 6, 19 | wb 195 | 1 wff (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) |
Colors of variables: wff setvar class |
This definition is referenced by: isoeq1 6467 isoeq2 6468 isoeq3 6469 isoeq4 6470 isoeq5 6471 nfiso 6472 isof1o 6473 isof1oidb 6474 isof1oopb 6475 isorel 6476 soisores 6477 soisoi 6478 isoid 6479 isocnv 6480 isocnv2 6481 isocnv3 6482 isores2 6483 isores3 6485 isotr 6486 isoini2 6489 f1oiso 6501 f1owe 6503 smoiso2 7353 alephiso 8804 compssiso 9079 negiso 10880 om2uzisoi 12615 icopnfhmeo 22550 reefiso 24006 logltb 24150 isoun 28862 xrmulc1cn 29304 wepwsolem 36630 iso0 37528 fourierdlem54 39053 |
Copyright terms: Public domain | W3C validator |