New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > df-iso | 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 SF, 5-Jan-2015.) |
Ref | Expression |
---|---|
df-iso |
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 4782 | . 2 |
7 | 1, 2, 5 | wf1o 4780 | . . 3 |
8 | vx | . . . . . . . 8 | |
9 | 8 | cv 1641 | . . . . . . 7 |
10 | vy | . . . . . . . 8 | |
11 | 10 | cv 1641 | . . . . . . 7 |
12 | 9, 11, 3 | wbr 4639 | . . . . . 6 |
13 | 9, 5 | cfv 4781 | . . . . . . 7 |
14 | 11, 5 | cfv 4781 | . . . . . . 7 |
15 | 13, 14, 4 | wbr 4639 | . . . . . 6 |
16 | 12, 15 | wb 176 | . . . . 5 |
17 | 16, 10, 1 | wral 2614 | . . . 4 |
18 | 17, 8, 1 | wral 2614 | . . 3 |
19 | 7, 18 | wa 358 | . 2 |
20 | 6, 19 | wb 176 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: isoeq1 5482 isoeq2 5483 isoeq3 5484 isoeq4 5485 isoeq5 5486 nfiso 5487 isof1o 5488 isorel 5489 isoid 5490 isocnv 5491 isocnv2 5492 isores2 5493 isotr 5495 isoini2 5498 f1oiso 5499 |
Copyright terms: Public domain | W3C validator |