Theorem coindi

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

	Ref	Expression
Assertion	coindi	⊢ ( ( ◡ 𝐹 ∘ 𝐹 ) ⊆ I → ( 𝐹 ∘ ( 𝐴 ∩ 𝐵 ) ) = ( ( 𝐹 ∘ 𝐴 ) ∩ ( 𝐹 ∘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		coindiss	⊢ ( 𝐹 ∘ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( 𝐹 ∘ 𝐴 ) ∩ ( 𝐹 ∘ 𝐵 ) )
2	1	a1i	⊢ ( ( ◡ 𝐹 ∘ 𝐹 ) ⊆ I → ( 𝐹 ∘ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( 𝐹 ∘ 𝐴 ) ∩ ( 𝐹 ∘ 𝐵 ) ) )
3		comodular	⊢ ( ( 𝐹 ∘ 𝐴 ) ∩ ( 𝐹 ∘ 𝐵 ) ) ⊆ ( ( 𝐹 ∩ ( ( 𝐹 ∘ 𝐵 ) ∘ ◡ 𝐴 ) ) ∘ ( 𝐴 ∩ ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐵 ) ) ) )
4		inss1	⊢ ( 𝐹 ∩ ( ( 𝐹 ∘ 𝐵 ) ∘ ◡ 𝐴 ) ) ⊆ 𝐹
5	4	a1i	⊢ ( ( ◡ 𝐹 ∘ 𝐹 ) ⊆ I → ( 𝐹 ∩ ( ( 𝐹 ∘ 𝐵 ) ∘ ◡ 𝐴 ) ) ⊆ 𝐹 )
6		coass	⊢ ( ( ◡ 𝐹 ∘ 𝐹 ) ∘ 𝐵 ) = ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐵 ) )
7		coss1	⊢ ( ( ◡ 𝐹 ∘ 𝐹 ) ⊆ I → ( ( ◡ 𝐹 ∘ 𝐹 ) ∘ 𝐵 ) ⊆ ( I ∘ 𝐵 ) )
8		coi2ss	⊢ ( I ∘ 𝐵 ) ⊆ 𝐵
9	7 8	sstrdi	⊢ ( ( ◡ 𝐹 ∘ 𝐹 ) ⊆ I → ( ( ◡ 𝐹 ∘ 𝐹 ) ∘ 𝐵 ) ⊆ 𝐵 )
10	6 9	eqsstrrid	⊢ ( ( ◡ 𝐹 ∘ 𝐹 ) ⊆ I → ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐵 ) ) ⊆ 𝐵 )
11		sslin	⊢ ( ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐵 ) ) ⊆ 𝐵 → ( 𝐴 ∩ ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐵 ) ) ) ⊆ ( 𝐴 ∩ 𝐵 ) )
12	10 11	syl	⊢ ( ( ◡ 𝐹 ∘ 𝐹 ) ⊆ I → ( 𝐴 ∩ ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐵 ) ) ) ⊆ ( 𝐴 ∩ 𝐵 ) )
13	5 12	coss12d	⊢ ( ( ◡ 𝐹 ∘ 𝐹 ) ⊆ I → ( ( 𝐹 ∩ ( ( 𝐹 ∘ 𝐵 ) ∘ ◡ 𝐴 ) ) ∘ ( 𝐴 ∩ ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐵 ) ) ) ) ⊆ ( 𝐹 ∘ ( 𝐴 ∩ 𝐵 ) ) )
14	3 13	sstrid	⊢ ( ( ◡ 𝐹 ∘ 𝐹 ) ⊆ I → ( ( 𝐹 ∘ 𝐴 ) ∩ ( 𝐹 ∘ 𝐵 ) ) ⊆ ( 𝐹 ∘ ( 𝐴 ∩ 𝐵 ) ) )
15	2 14	eqssd	⊢ ( ( ◡ 𝐹 ∘ 𝐹 ) ⊆ I → ( 𝐹 ∘ ( 𝐴 ∩ 𝐵 ) ) = ( ( 𝐹 ∘ 𝐴 ) ∩ ( 𝐹 ∘ 𝐵 ) ) )