Theorem coindir 38210

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

Assertion

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

Proof of Theorem coindir

Step	Hyp	Ref	Expression
1		coindirss 38199	. . 3 ⊢ ((𝐴 ∩ 𝐵) ∘ 𝐹) ⊆ ((𝐴 ∘ 𝐹) ∩ (𝐵 ∘ 𝐹))
2	1	a1i 11	. 2 ⊢ ((𝐹 ∘ ◡𝐹) ⊆ I → ((𝐴 ∩ 𝐵) ∘ 𝐹) ⊆ ((𝐴 ∘ 𝐹) ∩ (𝐵 ∘ 𝐹)))
3		comodular 38200	. . 3 ⊢ ((𝐴 ∘ 𝐹) ∩ (𝐵 ∘ 𝐹)) ⊆ ((𝐴 ∩ ((𝐵 ∘ 𝐹) ∘ ◡𝐹)) ∘ (𝐹 ∩ (◡𝐴 ∘ (𝐵 ∘ 𝐹))))
4		coass 6288	. . . . . 6 ⊢ ((𝐵 ∘ 𝐹) ∘ ◡𝐹) = (𝐵 ∘ (𝐹 ∘ ◡𝐹))
5		coss2 5842	. . . . . . 7 ⊢ ((𝐹 ∘ ◡𝐹) ⊆ I → (𝐵 ∘ (𝐹 ∘ ◡𝐹)) ⊆ (𝐵 ∘ I ))
6		coi1ss 38194	. . . . . . 7 ⊢ (𝐵 ∘ I ) ⊆ 𝐵
7	5, 6	sstrdi 3925	. . . . . 6 ⊢ ((𝐹 ∘ ◡𝐹) ⊆ I → (𝐵 ∘ (𝐹 ∘ ◡𝐹)) ⊆ 𝐵)
8	4, 7	eqsstrid 3951	. . . . 5 ⊢ ((𝐹 ∘ ◡𝐹) ⊆ I → ((𝐵 ∘ 𝐹) ∘ ◡𝐹) ⊆ 𝐵)
9		sslin 4142	. . . . 5 ⊢ (((𝐵 ∘ 𝐹) ∘ ◡𝐹) ⊆ 𝐵 → (𝐴 ∩ ((𝐵 ∘ 𝐹) ∘ ◡𝐹)) ⊆ (𝐴 ∩ 𝐵))
10	8, 9	syl 18	. . . 4 ⊢ ((𝐹 ∘ ◡𝐹) ⊆ I → (𝐴 ∩ ((𝐵 ∘ 𝐹) ∘ ◡𝐹)) ⊆ (𝐴 ∩ 𝐵))
11		inss1 4136	. . . . 5 ⊢ (𝐹 ∩ (◡𝐴 ∘ (𝐵 ∘ 𝐹))) ⊆ 𝐹
12	11	a1i 11	. . . 4 ⊢ ((𝐹 ∘ ◡𝐹) ⊆ I → (𝐹 ∩ (◡𝐴 ∘ (𝐵 ∘ 𝐹))) ⊆ 𝐹)
13	10, 12	coss12d 5843	. . 3 ⊢ ((𝐹 ∘ ◡𝐹) ⊆ I → ((𝐴 ∩ ((𝐵 ∘ 𝐹) ∘ ◡𝐹)) ∘ (𝐹 ∩ (◡𝐴 ∘ (𝐵 ∘ 𝐹)))) ⊆ ((𝐴 ∩ 𝐵) ∘ 𝐹))
14	3, 13	sstrid 3924	. 2 ⊢ ((𝐹 ∘ ◡𝐹) ⊆ I → ((𝐴 ∘ 𝐹) ∩ (𝐵 ∘ 𝐹)) ⊆ ((𝐴 ∩ 𝐵) ∘ 𝐹))
15	2, 14	eqssd 3930	1 ⊢ ((𝐹 ∘ ◡𝐹) ⊆ I → ((𝐴 ∩ 𝐵) ∘ 𝐹) = ((𝐴 ∘ 𝐹) ∩ (𝐵 ∘ 𝐹)))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3900   ∩ cin 4092   I cid 5550  ^◡ccnv 5655   ∘ ccom 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pr 5396

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5172  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-res 5668

This theorem is used by: (None)