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	⊢ ( ( 𝐴 ∘ 𝐴 ) ⊆ I ↔ ( 𝐴 ∘ 𝐴 ) = ( I ↾ ( dom 𝐴 ∩ ran 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( ( 𝐴 ∘ 𝐴 ) ⊆ I → ( 𝐴 ∘ 𝐴 ) ⊆ I )
2		cossxp	⊢ ( 𝐴 ∘ 𝐴 ) ⊆ ( dom 𝐴 × ran 𝐴 )
3	2	a1i	⊢ ( ( 𝐴 ∘ 𝐴 ) ⊆ I → ( 𝐴 ∘ 𝐴 ) ⊆ ( dom 𝐴 × ran 𝐴 ) )
4	1 3	ssind	⊢ ( ( 𝐴 ∘ 𝐴 ) ⊆ I → ( 𝐴 ∘ 𝐴 ) ⊆ ( I ∩ ( dom 𝐴 × ran 𝐴 ) ) )
5		idinxpres	⊢ ( I ∩ ( dom 𝐴 × ran 𝐴 ) ) = ( I ↾ ( dom 𝐴 ∩ ran 𝐴 ) )
6	4 5	sseqtrdi	⊢ ( ( 𝐴 ∘ 𝐴 ) ⊆ I → ( 𝐴 ∘ 𝐴 ) ⊆ ( I ↾ ( dom 𝐴 ∩ ran 𝐴 ) ) )
7		cossididres	⊢ ( ( 𝐴 ∘ 𝐴 ) ⊆ I → ( I ↾ ( dom 𝐴 ∩ ran 𝐴 ) ) ⊆ ( 𝐴 ∘ 𝐴 ) )
8	6 7	eqssd	⊢ ( ( 𝐴 ∘ 𝐴 ) ⊆ I → ( 𝐴 ∘ 𝐴 ) = ( I ↾ ( dom 𝐴 ∩ ran 𝐴 ) ) )
9		id	⊢ ( ( 𝐴 ∘ 𝐴 ) = ( I ↾ ( dom 𝐴 ∩ ran 𝐴 ) ) → ( 𝐴 ∘ 𝐴 ) = ( I ↾ ( dom 𝐴 ∩ ran 𝐴 ) ) )
10		resss	⊢ ( I ↾ ( dom 𝐴 ∩ ran 𝐴 ) ) ⊆ I
11	9 10	eqsstrdi	⊢ ( ( 𝐴 ∘ 𝐴 ) = ( I ↾ ( dom 𝐴 ∩ ran 𝐴 ) ) → ( 𝐴 ∘ 𝐴 ) ⊆ I )
12	8 11	impbii	⊢ ( ( 𝐴 ∘ 𝐴 ) ⊆ I ↔ ( 𝐴 ∘ 𝐴 ) = ( I ↾ ( dom 𝐴 ∩ ran 𝐴 ) ) )