Theorem nvo2

Description: A function from a class to itself is sub-involutive if and only if it is equal to its converse. (Contributed by BJ, 8-Nov-2026) Can shorten nvocnv .

	Ref	Expression
Assertion	nvo2	$$⊢B:X⟶X\to \left(B\circ B\subseteq \mathrm{I}\leftrightarrow B^{-1}=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(B:X⟶X\wedge B\circ B\subseteq \mathrm{I}\right)\to B\circ B\subseteq \mathrm{I}$$
2		simpl	$$⊢\left(B:X⟶X\wedge B\circ B\subseteq \mathrm{I}\right)\to B:X⟶X$$
3		frn	$$⊢B:X⟶X\to \mathrm{ran}B\subseteq X$$
4	2 3	syl	$$⊢\left(B:X⟶X\wedge B\circ B\subseteq \mathrm{I}\right)\to \mathrm{ran}B\subseteq X$$
5		fdm	$$⊢B:X⟶X\to \mathrm{dom}B=X$$
6	2 5	syl	$$⊢\left(B:X⟶X\wedge B\circ B\subseteq \mathrm{I}\right)\to \mathrm{dom}B=X$$
7	4 6	sseqtrrd	$$⊢\left(B:X⟶X\wedge B\circ B\subseteq \mathrm{I}\right)\to \mathrm{ran}B\subseteq \mathrm{dom}B$$
8	1 7	jca	$$⊢\left(B:X⟶X\wedge B\circ B\subseteq \mathrm{I}\right)\to \left(B\circ B\subseteq \mathrm{I}\wedge \mathrm{ran}B\subseteq \mathrm{dom}B\right)$$
9		cossidcnvss	$$⊢\left(B\circ B\subseteq \mathrm{I}\wedge \mathrm{ran}B\subseteq \mathrm{dom}B\right)\leftrightarrow \left(B^{-1}\subseteq B\wedge B\circ B^{-1}\subseteq \mathrm{I}\right)$$
10	8 9	sylib	$$⊢\left(B:X⟶X\wedge B\circ B\subseteq \mathrm{I}\right)\to \left(B^{-1}\subseteq B\wedge B\circ B^{-1}\subseteq \mathrm{I}\right)$$
11	10	simpld	$$⊢\left(B:X⟶X\wedge B\circ B\subseteq \mathrm{I}\right)\to B^{-1}\subseteq B$$
12		frel	$$⊢B:X⟶X\to \mathrm{Rel}B$$
13	2 12	syl	$$⊢\left(B:X⟶X\wedge B\circ B\subseteq \mathrm{I}\right)\to \mathrm{Rel}B$$
14		dfrel2	$$⊢\mathrm{Rel}B\leftrightarrow {B^{-1}}^{-1}=B$$
15	13 14	sylib	$$⊢\left(B:X⟶X\wedge B\circ B\subseteq \mathrm{I}\right)\to {B^{-1}}^{-1}=B$$
16		cnvss	$$⊢B^{-1}\subseteq B\to {B^{-1}}^{-1}\subseteq B^{-1}$$
17	11 16	syl	$$⊢\left(B:X⟶X\wedge B\circ B\subseteq \mathrm{I}\right)\to {B^{-1}}^{-1}\subseteq B^{-1}$$
18	15 17	eqsstrrd	$$⊢\left(B:X⟶X\wedge B\circ B\subseteq \mathrm{I}\right)\to B\subseteq B^{-1}$$
19	11 18	eqssd	$$⊢\left(B:X⟶X\wedge B\circ B\subseteq \mathrm{I}\right)\to B^{-1}=B$$
20		simpr	$$⊢\left(B:X⟶X\wedge B^{-1}=B\right)\to B^{-1}=B$$
21	20	eqimssd	$$⊢\left(B:X⟶X\wedge B^{-1}=B\right)\to B^{-1}\subseteq B$$
22		simpl	$$⊢\left(B:X⟶X\wedge B^{-1}=B\right)\to B:X⟶X$$
23		ffun	$$⊢B:X⟶X\to \mathrm{Fun}B$$
24	22 23	syl	$$⊢\left(B:X⟶X\wedge B^{-1}=B\right)\to \mathrm{Fun}B$$
25		df-fun	$$⊢\mathrm{Fun}B\leftrightarrow \left(\mathrm{Rel}B\wedge B\circ B^{-1}\subseteq \mathrm{I}\right)$$
26	25	simprbi	$$⊢\mathrm{Fun}B\to B\circ B^{-1}\subseteq \mathrm{I}$$
27	24 26	syl	$$⊢\left(B:X⟶X\wedge B^{-1}=B\right)\to B\circ B^{-1}\subseteq \mathrm{I}$$
28	21 27	jca	$$⊢\left(B:X⟶X\wedge B^{-1}=B\right)\to \left(B^{-1}\subseteq B\wedge B\circ B^{-1}\subseteq \mathrm{I}\right)$$
29	28 9	sylibr	$$⊢\left(B:X⟶X\wedge B^{-1}=B\right)\to \left(B\circ B\subseteq \mathrm{I}\wedge \mathrm{ran}B\subseteq \mathrm{dom}B\right)$$
30	29	simpld	$$⊢\left(B:X⟶X\wedge B^{-1}=B\right)\to B\circ B\subseteq \mathrm{I}$$
31	19 30	impbida	$$⊢B:X⟶X\to \left(B\circ B\subseteq \mathrm{I}\leftrightarrow B^{-1}=B\right)$$