Description: Precomposition is subdistributive over intersection. Compare with coundir . See coindir for equality when precomposing with a single-valued class. (Contributed by BJ, 8-Nov-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | coindirss | |- ( ( A i^i B ) o. C ) C_ ( ( A o. C ) i^i ( B o. C ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | inss1 | |- ( A i^i B ) C_ A |
|
| 2 | coss1 | |- ( ( A i^i B ) C_ A -> ( ( A i^i B ) o. C ) C_ ( A o. C ) ) |
|
| 3 | 1 2 | ax-mp | |- ( ( A i^i B ) o. C ) C_ ( A o. C ) |
| 4 | inss2 | |- ( A i^i B ) C_ B |
|
| 5 | coss1 | |- ( ( A i^i B ) C_ B -> ( ( A i^i B ) o. C ) C_ ( B o. C ) ) |
|
| 6 | 4 5 | ax-mp | |- ( ( A i^i B ) o. C ) C_ ( B o. C ) |
| 7 | 3 6 | ssini | |- ( ( A i^i B ) o. C ) C_ ( ( A o. C ) i^i ( B o. C ) ) |