coindi

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

		Ref	Expression
	Assertion	coindi	$⊢ F^{-1} \circ F \subseteq I \to F \circ (A \cap B) = (F \circ A) \cap (F \circ B)$

Step	Hyp	Ref	Expression
1		coindiss	$⊢ F \circ (A \cap B) \subseteq (F \circ A) \cap (F \circ B)$
2	1	a1i	$⊢ F^{-1} \circ F \subseteq I \to F \circ (A \cap B) \subseteq (F \circ A) \cap (F \circ B)$
3		comodular	$⊢ (F \circ A) \cap (F \circ B) \subseteq (F \cap ((F \circ B) \circ A^{-1})) \circ (A \cap (F^{-1} \circ (F \circ B)))$
4		inss1	$⊢ F \cap ((F \circ B) \circ A^{-1}) \subseteq F$
5	4	a1i	$⊢ F^{-1} \circ F \subseteq I \to F \cap ((F \circ B) \circ A^{-1}) \subseteq F$
6		coass	$⊢ (F^{-1} \circ F) \circ B = F^{-1} \circ (F \circ B)$
7		coss1	$⊢ F^{-1} \circ F \subseteq I \to (F^{-1} \circ F) \circ B \subseteq I \circ B$
8		coi2ss	$⊢ I \circ B \subseteq B$
9	7 8	sstrdi	$⊢ F^{-1} \circ F \subseteq I \to (F^{-1} \circ F) \circ B \subseteq B$
10	6 9	eqsstrrid	$⊢ F^{-1} \circ F \subseteq I \to F^{-1} \circ (F \circ B) \subseteq B$
11		sslin	$⊢ F^{-1} \circ (F \circ B) \subseteq B \to A \cap (F^{-1} \circ (F \circ B)) \subseteq A \cap B$
12	10 11	syl	$⊢ F^{-1} \circ F \subseteq I \to A \cap (F^{-1} \circ (F \circ B)) \subseteq A \cap B$
13	5 12	coss12d	$⊢ F^{-1} \circ F \subseteq I \to (F \cap ((F \circ B) \circ A^{-1})) \circ (A \cap (F^{-1} \circ (F \circ B))) \subseteq F \circ (A \cap B)$
14	3 13	sstrid	$⊢ F^{-1} \circ F \subseteq I \to (F \circ A) \cap (F \circ B) \subseteq F \circ (A \cap B)$
15	2 14	eqssd	$⊢ F^{-1} \circ F \subseteq I \to F \circ (A \cap B) = (F \circ A) \cap (F \circ B)$

Metamath Proof Explorer