![]() |
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 6218 | . 2 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) |
7 | 1, 2, 5 | wf1o 6216 | . . 3 wff 𝐻:𝐴–1-1-onto→𝐵 |
8 | vx | . . . . . . . 8 setvar 𝑥 | |
9 | 8 | cv 1519 | . . . . . . 7 class 𝑥 |
10 | vy | . . . . . . . 8 setvar 𝑦 | |
11 | 10 | cv 1519 | . . . . . . 7 class 𝑦 |
12 | 9, 11, 3 | wbr 4956 | . . . . . 6 wff 𝑥𝑅𝑦 |
13 | 9, 5 | cfv 6217 | . . . . . . 7 class (𝐻‘𝑥) |
14 | 11, 5 | cfv 6217 | . . . . . . 7 class (𝐻‘𝑦) |
15 | 13, 14, 4 | wbr 4956 | . . . . . 6 wff (𝐻‘𝑥)𝑆(𝐻‘𝑦) |
16 | 12, 15 | wb 207 | . . . . 5 wff (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) |
17 | 16, 10, 1 | wral 3103 | . . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) |
18 | 17, 8, 1 | wral 3103 | . . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) |
19 | 7, 18 | wa 396 | . 2 wff (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) |
20 | 6, 19 | wb 207 | 1 wff (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) |
Colors of variables: wff setvar class |
This definition is referenced by: isoeq1 6924 isoeq2 6925 isoeq3 6926 isoeq4 6927 isoeq5 6928 nfiso 6929 isof1o 6930 isof1oidb 6931 isof1oopb 6932 isorel 6933 soisores 6934 soisoi 6935 isoid 6936 isocnv 6937 isocnv2 6938 isocnv3 6939 isores2 6940 isores3 6942 isotr 6943 isoini2 6946 f1oiso 6958 f1owe 6960 smoiso2 7849 alephiso 9359 compssiso 9631 negiso 11458 om2uzisoi 13160 icopnfhmeo 23218 reefiso 24707 logltb 24852 isoun 30098 xrmulc1cn 30746 wepwsolem 39078 alephiso2 39353 iso0 40129 fourierdlem54 41941 rrx2plordisom 44145 |
Copyright terms: Public domain | W3C validator |