Theorem coindir

Description: Precomposition with a single-valued class (see cocnv2ssid ) distributes over intersection. (Contributed by BJ, 7-Nov-2026)

	Ref	Expression
Assertion	coindir	|- ( ( F o. `' F ) C_ _I -> ( ( A i^i B ) o. F ) = ( ( A o. F ) i^i ( B o. F ) ) )

Proof

Step	Hyp	Ref	Expression
1		coindirss	|- ( ( A i^i B ) o. F ) C_ ( ( A o. F ) i^i ( B o. F ) )
2	1	a1i	|- ( ( F o. `' F ) C_ _I -> ( ( A i^i B ) o. F ) C_ ( ( A o. F ) i^i ( B o. F ) ) )
3		comodular	|- ( ( A o. F ) i^i ( B o. F ) ) C_ ( ( A i^i ( ( B o. F ) o. `' F ) ) o. ( F i^i ( `' A o. ( B o. F ) ) ) )
4		coass	|- ( ( B o. F ) o. `' F ) = ( B o. ( F o. `' F ) )
5		coss2	|- ( ( F o. `' F ) C_ _I -> ( B o. ( F o. `' F ) ) C_ ( B o. _I ) )
6		coi1ss	|- ( B o. _I ) C_ B
7	5 6	sstrdi	|- ( ( F o. `' F ) C_ _I -> ( B o. ( F o. `' F ) ) C_ B )
8	4 7	eqsstrid	|- ( ( F o. `' F ) C_ _I -> ( ( B o. F ) o. `' F ) C_ B )
9		sslin	|- ( ( ( B o. F ) o. `' F ) C_ B -> ( A i^i ( ( B o. F ) o. `' F ) ) C_ ( A i^i B ) )
10	8 9	syl	|- ( ( F o. `' F ) C_ _I -> ( A i^i ( ( B o. F ) o. `' F ) ) C_ ( A i^i B ) )
11		inss1	|- ( F i^i ( `' A o. ( B o. F ) ) ) C_ F
12	11	a1i	|- ( ( F o. `' F ) C_ _I -> ( F i^i ( `' A o. ( B o. F ) ) ) C_ F )
13	10 12	coss12d	|- ( ( F o. `' F ) C_ _I -> ( ( A i^i ( ( B o. F ) o. `' F ) ) o. ( F i^i ( `' A o. ( B o. F ) ) ) ) C_ ( ( A i^i B ) o. F ) )
14	3 13	sstrid	|- ( ( F o. `' F ) C_ _I -> ( ( A o. F ) i^i ( B o. F ) ) C_ ( ( A i^i B ) o. F ) )
15	2 14	eqssd	|- ( ( F o. `' F ) C_ _I -> ( ( A i^i B ) o. F ) = ( ( A o. F ) i^i ( B o. F ) ) )