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 5199 | . 2 |
7 | 1, 2, 5 | wf1o 5197 | . . 3 |
8 | vx | . . . . . . . 8 | |
9 | 8 | cv 1347 | . . . . . . 7 |
10 | vy | . . . . . . . 8 | |
11 | 10 | cv 1347 | . . . . . . 7 |
12 | 9, 11, 3 | wbr 3989 | . . . . . 6 |
13 | 9, 5 | cfv 5198 | . . . . . . 7 |
14 | 11, 5 | cfv 5198 | . . . . . . 7 |
15 | 13, 14, 4 | wbr 3989 | . . . . . 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 5780 isoeq2 5781 isoeq3 5782 isoeq4 5783 isoeq5 5784 nfiso 5785 isof1o 5786 isorel 5787 isoid 5789 isocnv 5790 isocnv2 5791 isores2 5792 isores3 5794 isotr 5795 iso0 5796 isoini2 5798 f1oiso 5805 negiso 8871 frec2uzisod 10363 zfz1isolem1 10775 xrnegiso 11225 reefiso 13492 logltb 13589 |
Copyright terms: Public domain | W3C validator |