Theorem cossidmid

Description: If ( A o. B ) and ( C o. D ) are included in the identity relation and ( B o. C ) includes it on ( dom A i^i ran D ) , then ( A o. D ) is included in the identity relation. (Contributed by BJ, 8-Nov-2026)

	Ref	Expression
Assertion	cossidmid	⊢ ( ( ( 𝐴 ∘ 𝐵 ) ⊆ I ∧ ( 𝐶 ∘ 𝐷 ) ⊆ I ) → ( ( I ↾ ( dom 𝐴 ∩ ran 𝐷 ) ) ⊆ ( 𝐵 ∘ 𝐶 ) → ( 𝐴 ∘ 𝐷 ) ⊆ I ) )

Proof

Step	Hyp	Ref	Expression
1		coidmid	⊢ ( ( I ↾ ( dom 𝐴 ∩ ran 𝐷 ) ) ⊆ ( 𝐵 ∘ 𝐶 ) → ( 𝐴 ∘ 𝐷 ) ⊆ ( ( 𝐴 ∘ 𝐵 ) ∘ ( 𝐶 ∘ 𝐷 ) ) )
2		simpl	⊢ ( ( ( 𝐴 ∘ 𝐵 ) ⊆ I ∧ ( 𝐶 ∘ 𝐷 ) ⊆ I ) → ( 𝐴 ∘ 𝐵 ) ⊆ I )
3		simpr	⊢ ( ( ( 𝐴 ∘ 𝐵 ) ⊆ I ∧ ( 𝐶 ∘ 𝐷 ) ⊆ I ) → ( 𝐶 ∘ 𝐷 ) ⊆ I )
4	2 3	coss12d	⊢ ( ( ( 𝐴 ∘ 𝐵 ) ⊆ I ∧ ( 𝐶 ∘ 𝐷 ) ⊆ I ) → ( ( 𝐴 ∘ 𝐵 ) ∘ ( 𝐶 ∘ 𝐷 ) ) ⊆ ( I ∘ I ) )
5		reli	⊢ Rel I
6		coi1	⊢ ( Rel I → ( I ∘ I ) = I )
7	5 6	ax-mp	⊢ ( I ∘ I ) = I
8	4 7	sseqtrdi	⊢ ( ( ( 𝐴 ∘ 𝐵 ) ⊆ I ∧ ( 𝐶 ∘ 𝐷 ) ⊆ I ) → ( ( 𝐴 ∘ 𝐵 ) ∘ ( 𝐶 ∘ 𝐷 ) ) ⊆ I )
9	1 8	sylan9ssr	⊢ ( ( ( ( 𝐴 ∘ 𝐵 ) ⊆ I ∧ ( 𝐶 ∘ 𝐷 ) ⊆ I ) ∧ ( I ↾ ( dom 𝐴 ∩ ran 𝐷 ) ) ⊆ ( 𝐵 ∘ 𝐶 ) ) → ( 𝐴 ∘ 𝐷 ) ⊆ I )
10	9	ex	⊢ ( ( ( 𝐴 ∘ 𝐵 ) ⊆ I ∧ ( 𝐶 ∘ 𝐷 ) ⊆ I ) → ( ( I ↾ ( dom 𝐴 ∩ ran 𝐷 ) ) ⊆ ( 𝐵 ∘ 𝐶 ) → ( 𝐴 ∘ 𝐷 ) ⊆ I ) )