Theorem coss1b

Description: Precomposition with a single-valued class (see cocnv2ssid ) preserves and reflects the subclass relation on its range. This is a generalization of the fact that surjections are right-cancellable. (Contributed by BJ, 24-Oct-2026) TODO: prove cocanss2 from it.

	Ref	Expression
Hypothesis	coss1b.1	⊢ ( 𝜑 → ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I )
Assertion	coss1b	⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) ↔ ( 𝐻 ↾ ran 𝐹 ) ⊆ ( 𝐾 ↾ ran 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		coss1b.1	⊢ ( 𝜑 → ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I )
2		coss1	⊢ ( ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) → ( ( 𝐻 ∘ 𝐹 ) ∘ ◡ 𝐹 ) ⊆ ( ( 𝐾 ∘ 𝐹 ) ∘ ◡ 𝐹 ) )
3		coass	⊢ ( ( 𝐻 ∘ 𝐹 ) ∘ ◡ 𝐹 ) = ( 𝐻 ∘ ( 𝐹 ∘ ◡ 𝐹 ) )
4		iss	⊢ ( ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I ↔ ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ dom ( 𝐹 ∘ ◡ 𝐹 ) ) )
5	1 4	sylib	⊢ ( 𝜑 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ dom ( 𝐹 ∘ ◡ 𝐹 ) ) )
6		dmcocnv2	⊢ dom ( 𝐹 ∘ ◡ 𝐹 ) = ran 𝐹
7	6	reseq2i	⊢ ( I ↾ dom ( 𝐹 ∘ ◡ 𝐹 ) ) = ( I ↾ ran 𝐹 )
8	5 7	eqtrdi	⊢ ( 𝜑 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ran 𝐹 ) )
9	8	coeq2d	⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐹 ∘ ◡ 𝐹 ) ) = ( 𝐻 ∘ ( I ↾ ran 𝐹 ) ) )
10		coires1	⊢ ( 𝐻 ∘ ( I ↾ ran 𝐹 ) ) = ( 𝐻 ↾ ran 𝐹 )
11	9 10	eqtrdi	⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐹 ∘ ◡ 𝐹 ) ) = ( 𝐻 ↾ ran 𝐹 ) )
12	3 11	eqtrid	⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐹 ) ∘ ◡ 𝐹 ) = ( 𝐻 ↾ ran 𝐹 ) )
13		coass	⊢ ( ( 𝐾 ∘ 𝐹 ) ∘ ◡ 𝐹 ) = ( 𝐾 ∘ ( 𝐹 ∘ ◡ 𝐹 ) )
14	8	coeq2d	⊢ ( 𝜑 → ( 𝐾 ∘ ( 𝐹 ∘ ◡ 𝐹 ) ) = ( 𝐾 ∘ ( I ↾ ran 𝐹 ) ) )
15		coires1	⊢ ( 𝐾 ∘ ( I ↾ ran 𝐹 ) ) = ( 𝐾 ↾ ran 𝐹 )
16	14 15	eqtrdi	⊢ ( 𝜑 → ( 𝐾 ∘ ( 𝐹 ∘ ◡ 𝐹 ) ) = ( 𝐾 ↾ ran 𝐹 ) )
17	13 16	eqtrid	⊢ ( 𝜑 → ( ( 𝐾 ∘ 𝐹 ) ∘ ◡ 𝐹 ) = ( 𝐾 ↾ ran 𝐹 ) )
18	12 17	sseq12d	⊢ ( 𝜑 → ( ( ( 𝐻 ∘ 𝐹 ) ∘ ◡ 𝐹 ) ⊆ ( ( 𝐾 ∘ 𝐹 ) ∘ ◡ 𝐹 ) ↔ ( 𝐻 ↾ ran 𝐹 ) ⊆ ( 𝐾 ↾ ran 𝐹 ) ) )
19	2 18	imbitrid	⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) → ( 𝐻 ↾ ran 𝐹 ) ⊆ ( 𝐾 ↾ ran 𝐹 ) ) )
20		coss1	⊢ ( ( 𝐻 ↾ ran 𝐹 ) ⊆ ( 𝐾 ↾ ran 𝐹 ) → ( ( 𝐻 ↾ ran 𝐹 ) ∘ 𝐹 ) ⊆ ( ( 𝐾 ↾ ran 𝐹 ) ∘ 𝐹 ) )
21		coresrn	⊢ ( ( 𝐻 ↾ ran 𝐹 ) ∘ 𝐹 ) = ( 𝐻 ∘ 𝐹 )
22		coresrn	⊢ ( ( 𝐾 ↾ ran 𝐹 ) ∘ 𝐹 ) = ( 𝐾 ∘ 𝐹 )
23	20 21 22	3sstr3g	⊢ ( ( 𝐻 ↾ ran 𝐹 ) ⊆ ( 𝐾 ↾ ran 𝐹 ) → ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) )
24	19 23	impbid1	⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) ↔ ( 𝐻 ↾ ran 𝐹 ) ⊆ ( 𝐾 ↾ ran 𝐹 ) ) )