Metamath Proof Explorer

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 = ( dom A i^i ran A )
Assertion nvo3 
|- ( ( A o. A ) C_ _I <-> ( ( A |` X ) : X -1-1-onto-> X /\ ( `' A |` X ) = ( A |` X ) ) )

Proof

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