Theorem coindi

Description: Postcomposition with an injective class (see cocnv1ssid ) distributes over intersection. (Contributed by BJ, 8-Nov-2026)

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

Proof

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