Description: Define the class of all converse reflexive sets, see the comment of df-ssr . It is used only by df-cnvrefrels . (Contributed by Peter Mazsa, 22-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | df-cnvrefs | |- CnvRefs = { x | ( _I i^i ( dom x X. ran x ) ) `' _S ( x i^i ( dom x X. ran x ) ) } |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | ccnvrefs | |- CnvRefs |
|
1 | vx | |- x |
|
2 | cid | |- _I |
|
3 | 1 | cv | |- x |
4 | 3 | cdm | |- dom x |
5 | 3 | crn | |- ran x |
6 | 4 5 | cxp | |- ( dom x X. ran x ) |
7 | 2 6 | cin | |- ( _I i^i ( dom x X. ran x ) ) |
8 | cssr | |- _S |
|
9 | 8 | ccnv | |- `' _S |
10 | 3 6 | cin | |- ( x i^i ( dom x X. ran x ) ) |
11 | 7 10 9 | wbr | |- ( _I i^i ( dom x X. ran x ) ) `' _S ( x i^i ( dom x X. ran x ) ) |
12 | 11 1 | cab | |- { x | ( _I i^i ( dom x X. ran x ) ) `' _S ( x i^i ( dom x X. ran x ) ) } |
13 | 0 12 | wceq | |- CnvRefs = { x | ( _I i^i ( dom x X. ran x ) ) `' _S ( x i^i ( dom x X. ran x ) ) } |