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 | ⊢ 𝑋 ∈ V | |
| cocnv2ssidim.2 | ⊢ 𝑌 ∈ V | ||
| cocnv2ssidim.3 | ⊢ 𝑍 ∈ V | ||
| Assertion | cocnv2ssidim | ⊢ ( ( 𝑆 ∘ ◡ 𝑅 ) ⊆ I → ( ( 𝑋 𝑅 𝑌 ∧ 𝑋 𝑆 𝑍 ) → 𝑌 = 𝑍 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cocnv2ssidim.1 | ⊢ 𝑋 ∈ V | |
| 2 | cocnv2ssidim.2 | ⊢ 𝑌 ∈ V | |
| 3 | cocnv2ssidim.3 | ⊢ 𝑍 ∈ V | |
| 4 | 2 1 | brcnv | ⊢ ( 𝑌 ◡ 𝑅 𝑋 ↔ 𝑋 𝑅 𝑌 ) |
| 5 | 2 1 3 | brcoi | ⊢ ( ( 𝑌 ◡ 𝑅 𝑋 ∧ 𝑋 𝑆 𝑍 ) → 𝑌 ( 𝑆 ∘ ◡ 𝑅 ) 𝑍 ) |
| 6 | 4 5 | sylanbr | ⊢ ( ( 𝑋 𝑅 𝑌 ∧ 𝑋 𝑆 𝑍 ) → 𝑌 ( 𝑆 ∘ ◡ 𝑅 ) 𝑍 ) |
| 7 | ssbr | ⊢ ( ( 𝑆 ∘ ◡ 𝑅 ) ⊆ I → ( 𝑌 ( 𝑆 ∘ ◡ 𝑅 ) 𝑍 → 𝑌 I 𝑍 ) ) | |
| 8 | 3 | ideq | ⊢ ( 𝑌 I 𝑍 ↔ 𝑌 = 𝑍 ) |
| 9 | 7 8 | imbitrdi | ⊢ ( ( 𝑆 ∘ ◡ 𝑅 ) ⊆ I → ( 𝑌 ( 𝑆 ∘ ◡ 𝑅 ) 𝑍 → 𝑌 = 𝑍 ) ) |
| 10 | 6 9 | syl5 | ⊢ ( ( 𝑆 ∘ ◡ 𝑅 ) ⊆ I → ( ( 𝑋 𝑅 𝑌 ∧ 𝑋 𝑆 𝑍 ) → 𝑌 = 𝑍 ) ) |