![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-isom | 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 5218 | . 2 wff 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) |
7 | 1, 2, 5 | wf1o 5216 | . . 3 wff 𝐻:𝐴–1-1-onto→𝐵 |
8 | vx | . . . . . . . 8 setvar 𝑥 | |
9 | 8 | cv 1352 | . . . . . . 7 class 𝑥 |
10 | vy | . . . . . . . 8 setvar 𝑦 | |
11 | 10 | cv 1352 | . . . . . . 7 class 𝑦 |
12 | 9, 11, 3 | wbr 4004 | . . . . . 6 wff 𝑥𝑅𝑦 |
13 | 9, 5 | cfv 5217 | . . . . . . 7 class (𝐻‘𝑥) |
14 | 11, 5 | cfv 5217 | . . . . . . 7 class (𝐻‘𝑦) |
15 | 13, 14, 4 | wbr 4004 | . . . . . 6 wff (𝐻‘𝑥)𝑆(𝐻‘𝑦) |
16 | 12, 15 | wb 105 | . . . . 5 wff (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) |
17 | 16, 10, 1 | wral 2455 | . . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) |
18 | 17, 8, 1 | wral 2455 | . . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) |
19 | 7, 18 | wa 104 | . 2 wff (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) |
20 | 6, 19 | wb 105 | 1 wff (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) |
Colors of variables: wff set class |
This definition is referenced by: isoeq1 5802 isoeq2 5803 isoeq3 5804 isoeq4 5805 isoeq5 5806 nfiso 5807 isof1o 5808 isorel 5809 isoid 5811 isocnv 5812 isocnv2 5813 isores2 5814 isores3 5816 isotr 5817 iso0 5818 isoini2 5820 f1oiso 5827 negiso 8912 frec2uzisod 10407 zfz1isolem1 10820 xrnegiso 11270 reefiso 14201 logltb 14298 |
Copyright terms: Public domain | W3C validator |