Theorem coindiss

Description: Postcomposition is subdistributive over intersection. Compare with coundi . See coindi for equality when postcomposing with an injective class. (Contributed by BJ, 8-Nov-2026)

	Ref	Expression
Assertion	coindiss	⊢ ( 𝐴 ∘ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( ( 𝐴 ∘ 𝐵 ) ∩ ( 𝐴 ∘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		inss1	⊢ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐵
2		coss2	⊢ ( ( 𝐵 ∩ 𝐶 ) ⊆ 𝐵 → ( 𝐴 ∘ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝐴 ∘ 𝐵 ) )
3	1 2	ax-mp	⊢ ( 𝐴 ∘ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝐴 ∘ 𝐵 )
4		inss2	⊢ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐶
5		coss2	⊢ ( ( 𝐵 ∩ 𝐶 ) ⊆ 𝐶 → ( 𝐴 ∘ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝐴 ∘ 𝐶 ) )
6	4 5	ax-mp	⊢ ( 𝐴 ∘ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝐴 ∘ 𝐶 )
7	3 6	ssini	⊢ ( 𝐴 ∘ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( ( 𝐴 ∘ 𝐵 ) ∩ ( 𝐴 ∘ 𝐶 ) )