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 o. A ) C_ _I <-> ( A o. A ) = ( _I |` ( dom A i^i ran A ) ) )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( ( A o. A ) C_ _I -> ( A o. A ) C_ _I )
2		cossxp	|- ( A o. A ) C_ ( dom A X. ran A )
3	2	a1i	|- ( ( A o. A ) C_ _I -> ( A o. A ) C_ ( dom A X. ran A ) )
4	1 3	ssind	|- ( ( A o. A ) C_ _I -> ( A o. A ) C_ ( _I i^i ( dom A X. ran A ) ) )
5		idinxpres	|- ( _I i^i ( dom A X. ran A ) ) = ( _I |` ( dom A i^i ran A ) )
6	4 5	sseqtrdi	|- ( ( A o. A ) C_ _I -> ( A o. A ) C_ ( _I |` ( dom A i^i ran A ) ) )
7		cossididres	|- ( ( A o. A ) C_ _I -> ( _I |` ( dom A i^i ran A ) ) C_ ( A o. A ) )
8	6 7	eqssd	|- ( ( A o. A ) C_ _I -> ( A o. A ) = ( _I |` ( dom A i^i ran A ) ) )
9		id	|- ( ( A o. A ) = ( _I |` ( dom A i^i ran A ) ) -> ( A o. A ) = ( _I |` ( dom A i^i ran A ) ) )
10		resss	|- ( _I |` ( dom A i^i ran A ) ) C_ _I
11	9 10	eqsstrdi	|- ( ( A o. A ) = ( _I |` ( dom A i^i ran A ) ) -> ( A o. A ) C_ _I )
12	8 11	impbii	|- ( ( A o. A ) C_ _I <-> ( A o. A ) = ( _I |` ( dom A i^i ran A ) ) )