Metamath Proof Explorer

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 -> ( ( B o. B ) C_ _I <-> `' B = B ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( B : X --> X /\ ( B o. B ) C_ _I ) -> ( B o. B ) C_ _I )
2 simpl 
 |-  ( ( B : X --> X /\ ( B o. B ) C_ _I ) -> B : X --> X )
3 frn 
 |-  ( B : X --> X -> ran B C_ X )
4 2 3 syl 
 |-  ( ( B : X --> X /\ ( B o. B ) C_ _I ) -> ran B C_ X )
5 fdm 
 |-  ( B : X --> X -> dom B = X )
6 2 5 syl 
 |-  ( ( B : X --> X /\ ( B o. B ) C_ _I ) -> dom B = X )
7 4 6 sseqtrrd 
 |-  ( ( B : X --> X /\ ( B o. B ) C_ _I ) -> ran B C_ dom B )
8 1 7 jca 
 |-  ( ( B : X --> X /\ ( B o. B ) C_ _I ) -> ( ( B o. B ) C_ _I /\ ran B C_ dom B ) )
9 cossidcnvss 
 |-  ( ( ( B o. B ) C_ _I /\ ran B C_ dom B ) <-> ( `' B C_ B /\ ( B o. `' B ) C_ _I ) )
10 8 9 sylib 
 |-  ( ( B : X --> X /\ ( B o. B ) C_ _I ) -> ( `' B C_ B /\ ( B o. `' B ) C_ _I ) )
11 10 simpld 
 |-  ( ( B : X --> X /\ ( B o. B ) C_ _I ) -> `' B C_ B )
12 frel 
 |-  ( B : X --> X -> Rel B )
13 2 12 syl 
 |-  ( ( B : X --> X /\ ( B o. B ) C_ _I ) -> Rel B )
14 dfrel2 
 |-  ( Rel B <-> `' `' B = B )
15 13 14 sylib 
 |-  ( ( B : X --> X /\ ( B o. B ) C_ _I ) -> `' `' B = B )
16 cnvss 
 |-  ( `' B C_ B -> `' `' B C_ `' B )
17 11 16 syl 
 |-  ( ( B : X --> X /\ ( B o. B ) C_ _I ) -> `' `' B C_ `' B )
18 15 17 eqsstrrd 
 |-  ( ( B : X --> X /\ ( B o. B ) C_ _I ) -> B C_ `' B )
19 11 18 eqssd 
 |-  ( ( B : X --> X /\ ( B o. B ) C_ _I ) -> `' B = B )
20 simpr 
 |-  ( ( B : X --> X /\ `' B = B ) -> `' B = B )
21 20 eqimssd 
 |-  ( ( B : X --> X /\ `' B = B ) -> `' B C_ B )
22 simpl 
 |-  ( ( B : X --> X /\ `' B = B ) -> B : X --> X )
23 ffun 
 |-  ( B : X --> X -> Fun B )
24 22 23 syl 
 |-  ( ( B : X --> X /\ `' B = B ) -> Fun B )
25 df-fun 
 |-  ( Fun B <-> ( Rel B /\ ( B o. `' B ) C_ _I ) )
26 25 simprbi 
 |-  ( Fun B -> ( B o. `' B ) C_ _I )
27 24 26 syl 
 |-  ( ( B : X --> X /\ `' B = B ) -> ( B o. `' B ) C_ _I )
28 21 27 jca 
 |-  ( ( B : X --> X /\ `' B = B ) -> ( `' B C_ B /\ ( B o. `' B ) C_ _I ) )
29 28 9 sylibr 
 |-  ( ( B : X --> X /\ `' B = B ) -> ( ( B o. B ) C_ _I /\ ran B C_ dom B ) )
30 29 simpld 
 |-  ( ( B : X --> X /\ `' B = B ) -> ( B o. B ) C_ _I )
31 19 30 impbida 
 |-  ( B : X --> X -> ( ( B o. B ) C_ _I <-> `' B = B ) )