Theorem nvo3

Description: A class is sub-involutive if and only if its restriction to the intersection of its domain and range is a bijection of that intersection onto itself and coincides with the restriction of its converse. (Contributed by BJ, 8-Nov-2026)

	Ref	Expression
Hypothesis	nvo3.def	$$⊢X=\mathrm{dom}A\cap \mathrm{ran}A$$
Assertion	nvo3	$$⊢A\circ A\subseteq \mathrm{I}\leftrightarrow \left(\left({A\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}X\wedge {A^{-1}\upharpoonright }_X={A\upharpoonright }_X\right)$$

Proof

Step	Hyp	Ref	Expression
1		nvo3.def	$$⊢X=\mathrm{dom}A\cap \mathrm{ran}A$$
2		relres	$$⊢\mathrm{Rel}\left({A\upharpoonright }_X\right)$$
3	2	a1i	$$⊢A\circ A\subseteq \mathrm{I}\to \mathrm{Rel}\left({A\upharpoonright }_X\right)$$
4		resss	$$⊢{A\upharpoonright }_X\subseteq A$$
5	4	a1i	$$⊢A\circ A\subseteq \mathrm{I}\to {A\upharpoonright }_X\subseteq A$$
6		inss2	$$⊢\mathrm{dom}A\cap \mathrm{ran}A\subseteq \mathrm{ran}A$$
7	1 6	eqsstri	$$⊢X\subseteq \mathrm{ran}A$$
8		ssres2	$$⊢X\subseteq \mathrm{ran}A\to {A\upharpoonright }_X\subseteq {A\upharpoonright }_{\mathrm{ran}A}$$
9	7 8	ax-mp	$$⊢{A\upharpoonright }_X\subseteq {A\upharpoonright }_{\mathrm{ran}A}$$
10		cossidres1	$$⊢A\circ A\subseteq \mathrm{I}\to {A\upharpoonright }_{\mathrm{ran}A}\subseteq A^{-1}$$
11	9 10	sstrid	$$⊢A\circ A\subseteq \mathrm{I}\to {A\upharpoonright }_X\subseteq A^{-1}$$
12		cnvss	$$⊢{A\upharpoonright }_X\subseteq A^{-1}\to {\left({A\upharpoonright }_X\right)}^{-1}\subseteq {A^{-1}}^{-1}$$
13	11 12	syl	$$⊢A\circ A\subseteq \mathrm{I}\to {\left({A\upharpoonright }_X\right)}^{-1}\subseteq {A^{-1}}^{-1}$$
14		cnvcnvss	$$⊢{A^{-1}}^{-1}\subseteq A$$
15	13 14	sstrdi	$$⊢A\circ A\subseteq \mathrm{I}\to {\left({A\upharpoonright }_X\right)}^{-1}\subseteq A$$
16	5 15	coss12d	$$⊢A\circ A\subseteq \mathrm{I}\to \left({A\upharpoonright }_X\right)\circ {\left({A\upharpoonright }_X\right)}^{-1}\subseteq A\circ A$$
17		id	$$⊢A\circ A\subseteq \mathrm{I}\to A\circ A\subseteq \mathrm{I}$$
18	16 17	sstrd	$$⊢A\circ A\subseteq \mathrm{I}\to \left({A\upharpoonright }_X\right)\circ {\left({A\upharpoonright }_X\right)}^{-1}\subseteq \mathrm{I}$$
19		df-fun	$$⊢\mathrm{Fun}\left({A\upharpoonright }_X\right)\leftrightarrow \left(\mathrm{Rel}\left({A\upharpoonright }_X\right)\wedge \left({A\upharpoonright }_X\right)\circ {\left({A\upharpoonright }_X\right)}^{-1}\subseteq \mathrm{I}\right)$$
20	3 18 19	sylanbrc	$$⊢A\circ A\subseteq \mathrm{I}\to \mathrm{Fun}\left({A\upharpoonright }_X\right)$$
21		inss1	$$⊢\mathrm{dom}A\cap \mathrm{ran}A\subseteq \mathrm{dom}A$$
22	1 21	eqsstri	$$⊢X\subseteq \mathrm{dom}A$$
23		ssdmres	$$⊢X\subseteq \mathrm{dom}A\leftrightarrow \mathrm{dom}\left({A\upharpoonright }_X\right)=X$$
24	22 23	mpbi	$$⊢\mathrm{dom}\left({A\upharpoonright }_X\right)=X$$
25	24	a1i	$$⊢A\circ A\subseteq \mathrm{I}\to \mathrm{dom}\left({A\upharpoonright }_X\right)=X$$
26		df-fn	$$⊢\left({A\upharpoonright }_X\right)FnX\leftrightarrow \left(\mathrm{Fun}\left({A\upharpoonright }_X\right)\wedge \mathrm{dom}\left({A\upharpoonright }_X\right)=X\right)$$
27	20 25 26	sylanbrc	$$⊢A\circ A\subseteq \mathrm{I}\to \left({A\upharpoonright }_X\right)FnX$$
28		rnss	$$⊢{A\upharpoonright }_X\subseteq A^{-1}\to \mathrm{ran}\left({A\upharpoonright }_X\right)\subseteq \mathrm{ran}{A}^{-1}$$
29	11 28	syl	$$⊢A\circ A\subseteq \mathrm{I}\to \mathrm{ran}\left({A\upharpoonright }_X\right)\subseteq \mathrm{ran}{A}^{-1}$$
30		dfdm4	$$⊢\mathrm{dom}A=\mathrm{ran}{A}^{-1}$$
31	29 30	sseqtrrdi	$$⊢A\circ A\subseteq \mathrm{I}\to \mathrm{ran}\left({A\upharpoonright }_X\right)\subseteq \mathrm{dom}A$$
32		rnresss	$$⊢\mathrm{ran}\left({A\upharpoonright }_X\right)\subseteq \mathrm{ran}A$$
33	32	a1i	$$⊢A\circ A\subseteq \mathrm{I}\to \mathrm{ran}\left({A\upharpoonright }_X\right)\subseteq \mathrm{ran}A$$
34	31 33	ssind	$$⊢A\circ A\subseteq \mathrm{I}\to \mathrm{ran}\left({A\upharpoonright }_X\right)\subseteq \mathrm{dom}A\cap \mathrm{ran}A$$
35	34 1	sseqtrrdi	$$⊢A\circ A\subseteq \mathrm{I}\to \mathrm{ran}\left({A\upharpoonright }_X\right)\subseteq X$$
36		df-f	$$⊢\left({A\upharpoonright }_X\right):X⟶X\leftrightarrow \left(\left({A\upharpoonright }_X\right)FnX\wedge \mathrm{ran}\left({A\upharpoonright }_X\right)\subseteq X\right)$$
37	27 35 36	sylanbrc	$$⊢A\circ A\subseteq \mathrm{I}\to \left({A\upharpoonright }_X\right):X⟶X$$
38		ffn	$$⊢\left({A\upharpoonright }_X\right):X⟶X\to \left({A\upharpoonright }_X\right)FnX$$
39	37 38	syl	$$⊢A\circ A\subseteq \mathrm{I}\to \left({A\upharpoonright }_X\right)FnX$$
40	5 5	coss12d	$$⊢A\circ A\subseteq \mathrm{I}\to \left({A\upharpoonright }_X\right)\circ \left({A\upharpoonright }_X\right)\subseteq A\circ A$$
41	40 17	sstrd	$$⊢A\circ A\subseteq \mathrm{I}\to \left({A\upharpoonright }_X\right)\circ \left({A\upharpoonright }_X\right)\subseteq \mathrm{I}$$
42		nvo2	$$⊢\left({A\upharpoonright }_X\right):X⟶X\to \left(\left({A\upharpoonright }_X\right)\circ \left({A\upharpoonright }_X\right)\subseteq \mathrm{I}\leftrightarrow {\left({A\upharpoonright }_X\right)}^{-1}={A\upharpoonright }_X\right)$$
43	37 42	syl	$$⊢A\circ A\subseteq \mathrm{I}\to \left(\left({A\upharpoonright }_X\right)\circ \left({A\upharpoonright }_X\right)\subseteq \mathrm{I}\leftrightarrow {\left({A\upharpoonright }_X\right)}^{-1}={A\upharpoonright }_X\right)$$
44	41 43	mpbid	$$⊢A\circ A\subseteq \mathrm{I}\to {\left({A\upharpoonright }_X\right)}^{-1}={A\upharpoonright }_X$$
45		nvof1o	$$⊢\left(\left({A\upharpoonright }_X\right)FnX\wedge {\left({A\upharpoonright }_X\right)}^{-1}={A\upharpoonright }_X\right)\to \left({A\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}X$$
46	39 44 45	syl2anc	$$⊢A\circ A\subseteq \mathrm{I}\to \left({A\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}X$$
47		residm	$$⊢{\left({A^{-1}\upharpoonright }_X\right)\upharpoonright }_X={A^{-1}\upharpoonright }_X$$
48		ssres2	$$⊢X\subseteq \mathrm{dom}A\to {A^{-1}\upharpoonright }_X\subseteq {A^{-1}\upharpoonright }_{\mathrm{dom}A}$$
49	22 48	ax-mp	$$⊢{A^{-1}\upharpoonright }_X\subseteq {A^{-1}\upharpoonright }_{\mathrm{dom}A}$$
50		cossidres2	$$⊢A\circ A\subseteq \mathrm{I}\to {A^{-1}\upharpoonright }_{\mathrm{dom}A}\subseteq A$$
51	49 50	sstrid	$$⊢A\circ A\subseteq \mathrm{I}\to {A^{-1}\upharpoonright }_X\subseteq A$$
52		ssres	$$⊢{A^{-1}\upharpoonright }_X\subseteq A\to {\left({A^{-1}\upharpoonright }_X\right)\upharpoonright }_X\subseteq {A\upharpoonright }_X$$
53	51 52	syl	$$⊢A\circ A\subseteq \mathrm{I}\to {\left({A^{-1}\upharpoonright }_X\right)\upharpoonright }_X\subseteq {A\upharpoonright }_X$$
54	47 53	eqsstrrid	$$⊢A\circ A\subseteq \mathrm{I}\to {A^{-1}\upharpoonright }_X\subseteq {A\upharpoonright }_X$$
55		residm	$$⊢{\left({A\upharpoonright }_X\right)\upharpoonright }_X={A\upharpoonright }_X$$
56		ssres	$$⊢{A\upharpoonright }_X\subseteq A^{-1}\to {\left({A\upharpoonright }_X\right)\upharpoonright }_X\subseteq {A^{-1}\upharpoonright }_X$$
57	11 56	syl	$$⊢A\circ A\subseteq \mathrm{I}\to {\left({A\upharpoonright }_X\right)\upharpoonright }_X\subseteq {A^{-1}\upharpoonright }_X$$
58	55 57	eqsstrrid	$$⊢A\circ A\subseteq \mathrm{I}\to {A\upharpoonright }_X\subseteq {A^{-1}\upharpoonright }_X$$
59	54 58	eqssd	$$⊢A\circ A\subseteq \mathrm{I}\to {A^{-1}\upharpoonright }_X={A\upharpoonright }_X$$
60	46 59	jca	$$⊢A\circ A\subseteq \mathrm{I}\to \left(\left({A\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}X\wedge {A^{-1}\upharpoonright }_X={A\upharpoonright }_X\right)$$
61		dmres	$$⊢\mathrm{dom}\left({A\upharpoonright }_X\right)=X\cap \mathrm{dom}A$$
62		inss1	$$⊢X\cap \mathrm{dom}A\subseteq X$$
63	61 62	eqsstri	$$⊢\mathrm{dom}\left({A\upharpoonright }_X\right)\subseteq X$$
64		cores2	$$⊢\mathrm{dom}\left({A\upharpoonright }_X\right)\subseteq X\to \left({A\upharpoonright }_X\right)\circ {\left({A^{-1}\upharpoonright }_X\right)}^{-1}=\left({A\upharpoonright }_X\right)\circ A$$
65	63 64	ax-mp	$$⊢\left({A\upharpoonright }_X\right)\circ {\left({A^{-1}\upharpoonright }_X\right)}^{-1}=\left({A\upharpoonright }_X\right)\circ A$$
66		incom	$$⊢\mathrm{dom}A\cap \mathrm{ran}A=\mathrm{ran}A\cap \mathrm{dom}A$$
67	1 66	eqtri	$$⊢X=\mathrm{ran}A\cap \mathrm{dom}A$$
68	67	reseq2i	$$⊢{A\upharpoonright }_X={A\upharpoonright }_{\left(\mathrm{ran}A\cap \mathrm{dom}A\right)}$$
69		resindm	$$⊢{A\upharpoonright }_{\left(\mathrm{ran}A\cap \mathrm{dom}A\right)}={A\upharpoonright }_{\mathrm{ran}A}$$
70	68 69	eqtri	$$⊢{A\upharpoonright }_X={A\upharpoonright }_{\mathrm{ran}A}$$
71	70	coeq1i	$$⊢\left({A\upharpoonright }_X\right)\circ A=\left({A\upharpoonright }_{\mathrm{ran}A}\right)\circ A$$
72		coresrn	$$⊢\left({A\upharpoonright }_{\mathrm{ran}A}\right)\circ A=A\circ A$$
73	71 72	eqtri	$$⊢\left({A\upharpoonright }_X\right)\circ A=A\circ A$$
74	65 73	eqtri	$$⊢\left({A\upharpoonright }_X\right)\circ {\left({A^{-1}\upharpoonright }_X\right)}^{-1}=A\circ A$$
75		simpr	$$⊢\left(\left({A\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}X\wedge {A^{-1}\upharpoonright }_X={A\upharpoonright }_X\right)\to {A^{-1}\upharpoonright }_X={A\upharpoonright }_X$$
76	75	cnveqd	$$⊢\left(\left({A\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}X\wedge {A^{-1}\upharpoonright }_X={A\upharpoonright }_X\right)\to {\left({A^{-1}\upharpoonright }_X\right)}^{-1}={\left({A\upharpoonright }_X\right)}^{-1}$$
77	76	coeq2d	$$⊢\left(\left({A\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}X\wedge {A^{-1}\upharpoonright }_X={A\upharpoonright }_X\right)\to \left({A\upharpoonright }_X\right)\circ {\left({A^{-1}\upharpoonright }_X\right)}^{-1}=\left({A\upharpoonright }_X\right)\circ {\left({A\upharpoonright }_X\right)}^{-1}$$
78		simpl	$$⊢\left(\left({A\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}X\wedge {A^{-1}\upharpoonright }_X={A\upharpoonright }_X\right)\to \left({A\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}X$$
79		f1ococnv2	$$⊢\left({A\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}X\to \left({A\upharpoonright }_X\right)\circ {\left({A\upharpoonright }_X\right)}^{-1}={\mathrm{I}\upharpoonright }_X$$
80	78 79	syl	$$⊢\left(\left({A\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}X\wedge {A^{-1}\upharpoonright }_X={A\upharpoonright }_X\right)\to \left({A\upharpoonright }_X\right)\circ {\left({A\upharpoonright }_X\right)}^{-1}={\mathrm{I}\upharpoonright }_X$$
81	77 80	eqtrd	$$⊢\left(\left({A\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}X\wedge {A^{-1}\upharpoonright }_X={A\upharpoonright }_X\right)\to \left({A\upharpoonright }_X\right)\circ {\left({A^{-1}\upharpoonright }_X\right)}^{-1}={\mathrm{I}\upharpoonright }_X$$
82	74 81	eqtr3id	$$⊢\left(\left({A\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}X\wedge {A^{-1}\upharpoonright }_X={A\upharpoonright }_X\right)\to A\circ A={\mathrm{I}\upharpoonright }_X$$
83		resss	$$⊢{\mathrm{I}\upharpoonright }_X\subseteq \mathrm{I}$$
84	82 83	eqsstrdi	$$⊢\left(\left({A\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}X\wedge {A^{-1}\upharpoonright }_X={A\upharpoonright }_X\right)\to A\circ A\subseteq \mathrm{I}$$
85	60 84	impbii	$$⊢A\circ A\subseteq \mathrm{I}\leftrightarrow \left(\left({A\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}X\wedge {A^{-1}\upharpoonright }_X={A\upharpoonright }_X\right)$$