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 5094 | . 2 |
7 | 1, 2, 5 | wf1o 5092 | . . 3 |
8 | vx | . . . . . . . 8 | |
9 | 8 | cv 1315 | . . . . . . 7 |
10 | vy | . . . . . . . 8 | |
11 | 10 | cv 1315 | . . . . . . 7 |
12 | 9, 11, 3 | wbr 3899 | . . . . . 6 |
13 | 9, 5 | cfv 5093 | . . . . . . 7 |
14 | 11, 5 | cfv 5093 | . . . . . . 7 |
15 | 13, 14, 4 | wbr 3899 | . . . . . 6 |
16 | 12, 15 | wb 104 | . . . . 5 |
17 | 16, 10, 1 | wral 2393 | . . . 4 |
18 | 17, 8, 1 | wral 2393 | . . 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 5670 isoeq2 5671 isoeq3 5672 isoeq4 5673 isoeq5 5674 nfiso 5675 isof1o 5676 isorel 5677 isoid 5679 isocnv 5680 isocnv2 5681 isores2 5682 isores3 5684 isotr 5685 iso0 5686 isoini2 5688 f1oiso 5695 negiso 8677 frec2uzisod 10135 zfz1isolem1 10538 xrnegiso 10986 |
Copyright terms: Public domain | W3C validator |