Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-isom | Unicode 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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | cR | . . 3 | |
4 | cS | . . 3 | |
5 | cH | . . 3 | |
6 | 1, 2, 3, 4, 5 | wiso 4903 | . 2 |
7 | 1, 2, 5 | wf1o 4901 | . . 3 |
8 | vx | . . . . . . . 8 | |
9 | 8 | cv 1242 | . . . . . . 7 |
10 | vy | . . . . . . . 8 | |
11 | 10 | cv 1242 | . . . . . . 7 |
12 | 9, 11, 3 | wbr 3764 | . . . . . 6 |
13 | 9, 5 | cfv 4902 | . . . . . . 7 |
14 | 11, 5 | cfv 4902 | . . . . . . 7 |
15 | 13, 14, 4 | wbr 3764 | . . . . . 6 |
16 | 12, 15 | wb 98 | . . . . 5 |
17 | 16, 10, 1 | wral 2306 | . . . 4 |
18 | 17, 8, 1 | wral 2306 | . . 3 |
19 | 7, 18 | wa 97 | . 2 |
20 | 6, 19 | wb 98 | 1 |
Colors of variables: wff set class |
This definition is referenced by: isoeq1 5441 isoeq2 5442 isoeq3 5443 isoeq4 5444 isoeq5 5445 nfiso 5446 isof1o 5447 isorel 5448 isoid 5450 isocnv 5451 isocnv2 5452 isores2 5453 isores3 5455 isotr 5456 isoini2 5458 f1oiso 5465 frec2uzisod 9193 |
Copyright terms: Public domain | W3C validator |