Theorem coss2b

Description: Postcomposition with an injective class (see cocnv1ssid ) preserves and reflects the subclass relation up to corestriction to its domain. This is a generalization of the fact that injections are left-cancellable. Compare with coss1b . There is no special syntax for corestriction as explained in the comment of df-res . (Contributed by BJ, 24-Oct-2026) TODO: prove cocanss1 from it.

	Ref	Expression
Hypothesis	coss2b.1	⊢ ( 𝜑 → ( ◡ 𝐹 ∘ 𝐹 ) ⊆ I )
Assertion	coss2b	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐻 ) ⊆ ( 𝐹 ∘ 𝐾 ) ↔ ( 𝐻 ∩ ( V × dom 𝐹 ) ) ⊆ ( 𝐾 ∩ ( V × dom 𝐹 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		coss2b.1	⊢ ( 𝜑 → ( ◡ 𝐹 ∘ 𝐹 ) ⊆ I )
2		coss2	⊢ ( ( 𝐹 ∘ 𝐻 ) ⊆ ( 𝐹 ∘ 𝐾 ) → ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐻 ) ) ⊆ ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐾 ) ) )
3		coass	⊢ ( ( ◡ 𝐹 ∘ 𝐹 ) ∘ 𝐻 ) = ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐻 ) )
4		iss	⊢ ( ( ◡ 𝐹 ∘ 𝐹 ) ⊆ I ↔ ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ dom ( ◡ 𝐹 ∘ 𝐹 ) ) )
5	1 4	sylib	⊢ ( 𝜑 → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ dom ( ◡ 𝐹 ∘ 𝐹 ) ) )
6		dmcocnv1	⊢ dom ( ◡ 𝐹 ∘ 𝐹 ) = dom 𝐹
7	6	reseq2i	⊢ ( I ↾ dom ( ◡ 𝐹 ∘ 𝐹 ) ) = ( I ↾ dom 𝐹 )
8	5 7	eqtrdi	⊢ ( 𝜑 → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ dom 𝐹 ) )
9	8	coeq1d	⊢ ( 𝜑 → ( ( ◡ 𝐹 ∘ 𝐹 ) ∘ 𝐻 ) = ( ( I ↾ dom 𝐹 ) ∘ 𝐻 ) )
10		coires2	⊢ ( ( I ↾ dom 𝐹 ) ∘ 𝐻 ) = ( 𝐻 ∩ ( V × dom 𝐹 ) )
11	9 10	eqtrdi	⊢ ( 𝜑 → ( ( ◡ 𝐹 ∘ 𝐹 ) ∘ 𝐻 ) = ( 𝐻 ∩ ( V × dom 𝐹 ) ) )
12	3 11	eqtr3id	⊢ ( 𝜑 → ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐻 ) ) = ( 𝐻 ∩ ( V × dom 𝐹 ) ) )
13		coass	⊢ ( ( ◡ 𝐹 ∘ 𝐹 ) ∘ 𝐾 ) = ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐾 ) )
14	8	coeq1d	⊢ ( 𝜑 → ( ( ◡ 𝐹 ∘ 𝐹 ) ∘ 𝐾 ) = ( ( I ↾ dom 𝐹 ) ∘ 𝐾 ) )
15		coires2	⊢ ( ( I ↾ dom 𝐹 ) ∘ 𝐾 ) = ( 𝐾 ∩ ( V × dom 𝐹 ) )
16	14 15	eqtrdi	⊢ ( 𝜑 → ( ( ◡ 𝐹 ∘ 𝐹 ) ∘ 𝐾 ) = ( 𝐾 ∩ ( V × dom 𝐹 ) ) )
17	13 16	eqtr3id	⊢ ( 𝜑 → ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐾 ) ) = ( 𝐾 ∩ ( V × dom 𝐹 ) ) )
18	12 17	sseq12d	⊢ ( 𝜑 → ( ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐻 ) ) ⊆ ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐾 ) ) ↔ ( 𝐻 ∩ ( V × dom 𝐹 ) ) ⊆ ( 𝐾 ∩ ( V × dom 𝐹 ) ) ) )
19	2 18	imbitrid	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐻 ) ⊆ ( 𝐹 ∘ 𝐾 ) → ( 𝐻 ∩ ( V × dom 𝐹 ) ) ⊆ ( 𝐾 ∩ ( V × dom 𝐹 ) ) ) )
20		coss2	⊢ ( ( 𝐻 ∩ ( V × dom 𝐹 ) ) ⊆ ( 𝐾 ∩ ( V × dom 𝐹 ) ) → ( 𝐹 ∘ ( 𝐻 ∩ ( V × dom 𝐹 ) ) ) ⊆ ( 𝐹 ∘ ( 𝐾 ∩ ( V × dom 𝐹 ) ) ) )
21		cnvrescnv	⊢ ◡ ( ◡ 𝐻 ↾ dom 𝐹 ) = ( 𝐻 ∩ ( V × dom 𝐹 ) )
22	21	coeq2i	⊢ ( 𝐹 ∘ ◡ ( ◡ 𝐻 ↾ dom 𝐹 ) ) = ( 𝐹 ∘ ( 𝐻 ∩ ( V × dom 𝐹 ) ) )
23		ssid	⊢ dom 𝐹 ⊆ dom 𝐹
24		cores2	⊢ ( dom 𝐹 ⊆ dom 𝐹 → ( 𝐹 ∘ ◡ ( ◡ 𝐻 ↾ dom 𝐹 ) ) = ( 𝐹 ∘ 𝐻 ) )
25	23 24	ax-mp	⊢ ( 𝐹 ∘ ◡ ( ◡ 𝐻 ↾ dom 𝐹 ) ) = ( 𝐹 ∘ 𝐻 )
26	22 25	eqtr3i	⊢ ( 𝐹 ∘ ( 𝐻 ∩ ( V × dom 𝐹 ) ) ) = ( 𝐹 ∘ 𝐻 )
27		cnvrescnv	⊢ ◡ ( ◡ 𝐾 ↾ dom 𝐹 ) = ( 𝐾 ∩ ( V × dom 𝐹 ) )
28	27	coeq2i	⊢ ( 𝐹 ∘ ◡ ( ◡ 𝐾 ↾ dom 𝐹 ) ) = ( 𝐹 ∘ ( 𝐾 ∩ ( V × dom 𝐹 ) ) )
29		cores2	⊢ ( dom 𝐹 ⊆ dom 𝐹 → ( 𝐹 ∘ ◡ ( ◡ 𝐾 ↾ dom 𝐹 ) ) = ( 𝐹 ∘ 𝐾 ) )
30	23 29	ax-mp	⊢ ( 𝐹 ∘ ◡ ( ◡ 𝐾 ↾ dom 𝐹 ) ) = ( 𝐹 ∘ 𝐾 )
31	28 30	eqtr3i	⊢ ( 𝐹 ∘ ( 𝐾 ∩ ( V × dom 𝐹 ) ) ) = ( 𝐹 ∘ 𝐾 )
32	20 26 31	3sstr3g	⊢ ( ( 𝐻 ∩ ( V × dom 𝐹 ) ) ⊆ ( 𝐾 ∩ ( V × dom 𝐹 ) ) → ( 𝐹 ∘ 𝐻 ) ⊆ ( 𝐹 ∘ 𝐾 ) )
33	19 32	impbid1	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐻 ) ⊆ ( 𝐹 ∘ 𝐾 ) ↔ ( 𝐻 ∩ ( V × dom 𝐹 ) ) ⊆ ( 𝐾 ∩ ( V × dom 𝐹 ) ) ) )