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 ⊢ 𝑋 = ( dom 𝐴 ∩ ran 𝐴 )
Assertion nvo3 ( ( 𝐴 ∘ 𝐴 ) ⊆ I ↔ ( ( 𝐴 ↾ 𝑋 ) : 𝑋 ⟶1-1onto 𝑋 ∧ ( ◡ 𝐴 ↾ 𝑋 ) = ( 𝐴 ↾ 𝑋 ) ) )

Proof

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