Theorem coindir

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

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

Proof

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