Theorem nvo

Description: Two ways to express "sub-involutivity" of a class, by which is meant involutivity on the intersection of the domain and range (see nvo3 ). (Contributed by BJ, 7-Nov-2026)

	Ref	Expression
Assertion	nvo	$$⊢A\circ A\subseteq \mathrm{I}\leftrightarrow A\circ A={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cap \mathrm{ran}A\right)}$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢A\circ A\subseteq \mathrm{I}\to A\circ A\subseteq \mathrm{I}$$
2		cossxp	$$⊢A\circ A\subseteq \mathrm{dom}A\times \mathrm{ran}A$$
3	2	a1i	$$⊢A\circ A\subseteq \mathrm{I}\to A\circ A\subseteq \mathrm{dom}A\times \mathrm{ran}A$$
4	1 3	ssind	$$⊢A\circ A\subseteq \mathrm{I}\to A\circ A\subseteq \mathrm{I}\cap \left(\mathrm{dom}A\times \mathrm{ran}A\right)$$
5		idinxpres	$$⊢\mathrm{I}\cap \left(\mathrm{dom}A\times \mathrm{ran}A\right)={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cap \mathrm{ran}A\right)}$$
6	4 5	sseqtrdi	$$⊢A\circ A\subseteq \mathrm{I}\to A\circ A\subseteq {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cap \mathrm{ran}A\right)}$$
7		cossididres	$$⊢A\circ A\subseteq \mathrm{I}\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cap \mathrm{ran}A\right)}\subseteq A\circ A$$
8	6 7	eqssd	$$⊢A\circ A\subseteq \mathrm{I}\to A\circ A={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cap \mathrm{ran}A\right)}$$
9		id	$$⊢A\circ A={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cap \mathrm{ran}A\right)}\to A\circ A={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cap \mathrm{ran}A\right)}$$
10		resss	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cap \mathrm{ran}A\right)}\subseteq \mathrm{I}$$
11	9 10	eqsstrdi	$$⊢A\circ A={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cap \mathrm{ran}A\right)}\to A\circ A\subseteq \mathrm{I}$$
12	8 11	impbii	$$⊢A\circ A\subseteq \mathrm{I}\leftrightarrow A\circ A={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cap \mathrm{ran}A\right)}$$