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 5119 | . 2 |
7 | 1, 2, 5 | wf1o 5117 | . . 3 |
8 | vx | . . . . . . . 8 | |
9 | 8 | cv 1330 | . . . . . . 7 |
10 | vy | . . . . . . . 8 | |
11 | 10 | cv 1330 | . . . . . . 7 |
12 | 9, 11, 3 | wbr 3924 | . . . . . 6 |
13 | 9, 5 | cfv 5118 | . . . . . . 7 |
14 | 11, 5 | cfv 5118 | . . . . . . 7 |
15 | 13, 14, 4 | wbr 3924 | . . . . . 6 |
16 | 12, 15 | wb 104 | . . . . 5 |
17 | 16, 10, 1 | wral 2414 | . . . 4 |
18 | 17, 8, 1 | wral 2414 | . . 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 5695 isoeq2 5696 isoeq3 5697 isoeq4 5698 isoeq5 5699 nfiso 5700 isof1o 5701 isorel 5702 isoid 5704 isocnv 5705 isocnv2 5706 isores2 5707 isores3 5709 isotr 5710 iso0 5711 isoini2 5713 f1oiso 5720 negiso 8706 frec2uzisod 10173 zfz1isolem1 10576 xrnegiso 11024 |
Copyright terms: Public domain | W3C validator |