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 4923 | . 2 |
7 | 1, 2, 5 | wf1o 4921 | . . 3 |
8 | vx | . . . . . . . 8 | |
9 | 8 | cv 1283 | . . . . . . 7 |
10 | vy | . . . . . . . 8 | |
11 | 10 | cv 1283 | . . . . . . 7 |
12 | 9, 11, 3 | wbr 3785 | . . . . . 6 |
13 | 9, 5 | cfv 4922 | . . . . . . 7 |
14 | 11, 5 | cfv 4922 | . . . . . . 7 |
15 | 13, 14, 4 | wbr 3785 | . . . . . 6 |
16 | 12, 15 | wb 103 | . . . . 5 |
17 | 16, 10, 1 | wral 2348 | . . . 4 |
18 | 17, 8, 1 | wral 2348 | . . 3 |
19 | 7, 18 | wa 102 | . 2 |
20 | 6, 19 | wb 103 | 1 |
Colors of variables: wff set class |
This definition is referenced by: isoeq1 5461 isoeq2 5462 isoeq3 5463 isoeq4 5464 isoeq5 5465 nfiso 5466 isof1o 5467 isorel 5468 isoid 5470 isocnv 5471 isocnv2 5472 isores2 5473 isores3 5475 isotr 5476 isoini2 5478 f1oiso 5485 negiso 8033 frec2uzisod 9409 |
Copyright terms: Public domain | W3C validator |