Description: Consequence of the composition of a class with a converse being included in the identity relation. The instance where the two classes are equal expresses single-valuedness. (Contributed by BJ, 24-Oct-2026) Note: can shorten fununiq .
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cocnv2ssidim.1 | |- X e. _V |
|
| cocnv2ssidim.2 | |- Y e. _V |
||
| cocnv2ssidim.3 | |- Z e. _V |
||
| Assertion | cocnv2ssidim | |- ( ( S o. `' R ) C_ _I -> ( ( X R Y /\ X S Z ) -> Y = Z ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cocnv2ssidim.1 | |- X e. _V |
|
| 2 | cocnv2ssidim.2 | |- Y e. _V |
|
| 3 | cocnv2ssidim.3 | |- Z e. _V |
|
| 4 | 2 1 | brcnv | |- ( Y `' R X <-> X R Y ) |
| 5 | 2 1 3 | brcoi | |- ( ( Y `' R X /\ X S Z ) -> Y ( S o. `' R ) Z ) |
| 6 | 4 5 | sylanbr | |- ( ( X R Y /\ X S Z ) -> Y ( S o. `' R ) Z ) |
| 7 | ssbr | |- ( ( S o. `' R ) C_ _I -> ( Y ( S o. `' R ) Z -> Y _I Z ) ) |
|
| 8 | 3 | ideq | |- ( Y _I Z <-> Y = Z ) |
| 9 | 7 8 | imbitrdi | |- ( ( S o. `' R ) C_ _I -> ( Y ( S o. `' R ) Z -> Y = Z ) ) |
| 10 | 6 9 | syl5 | |- ( ( S o. `' R ) C_ _I -> ( ( X R Y /\ X S Z ) -> Y = Z ) ) |