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 5197 | . 2 |
7 | 1, 2, 5 | wf1o 5195 | . . 3 |
8 | vx | . . . . . . . 8 | |
9 | 8 | cv 1347 | . . . . . . 7 |
10 | vy | . . . . . . . 8 | |
11 | 10 | cv 1347 | . . . . . . 7 |
12 | 9, 11, 3 | wbr 3987 | . . . . . 6 |
13 | 9, 5 | cfv 5196 | . . . . . . 7 |
14 | 11, 5 | cfv 5196 | . . . . . . 7 |
15 | 13, 14, 4 | wbr 3987 | . . . . . 6 |
16 | 12, 15 | wb 104 | . . . . 5 |
17 | 16, 10, 1 | wral 2448 | . . . 4 |
18 | 17, 8, 1 | wral 2448 | . . 3 |
19 | 7, 18 | wa 103 | . 2 |
20 | 6, 19 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: isoeq1 5778 isoeq2 5779 isoeq3 5780 isoeq4 5781 isoeq5 5782 nfiso 5783 isof1o 5784 isorel 5785 isoid 5787 isocnv 5788 isocnv2 5789 isores2 5790 isores3 5792 isotr 5793 iso0 5794 isoini2 5796 f1oiso 5803 negiso 8864 frec2uzisod 10356 zfz1isolem1 10768 xrnegiso 11218 reefiso 13457 logltb 13554 |
Copyright terms: Public domain | W3C validator |