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 ( 𝐵 : 𝑋 ⟶ 𝑋 → ( ( 𝐵 ∘ 𝐵 ) ⊆ I ↔ ◡ 𝐵 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ( 𝐵 ∘ 𝐵 ) ⊆ I ) → ( 𝐵 ∘ 𝐵 ) ⊆ I )
2 simpl ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ( 𝐵 ∘ 𝐵 ) ⊆ I ) → 𝐵 : 𝑋 ⟶ 𝑋 )
3 frn ⊢ ( 𝐵 : 𝑋 ⟶ 𝑋 → ran 𝐵 ⊆ 𝑋 )
4 2 3 syl ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ( 𝐵 ∘ 𝐵 ) ⊆ I ) → ran 𝐵 ⊆ 𝑋 )
5 fdm ⊢ ( 𝐵 : 𝑋 ⟶ 𝑋 → dom 𝐵 = 𝑋 )
6 2 5 syl ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ( 𝐵 ∘ 𝐵 ) ⊆ I ) → dom 𝐵 = 𝑋 )
7 4 6 sseqtrrd ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ( 𝐵 ∘ 𝐵 ) ⊆ I ) → ran 𝐵 ⊆ dom 𝐵 )
8 1 7 jca ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ( 𝐵 ∘ 𝐵 ) ⊆ I ) → ( ( 𝐵 ∘ 𝐵 ) ⊆ I ∧ ran 𝐵 ⊆ dom 𝐵 ) )
9 cossidcnvss ⊢ ( ( ( 𝐵 ∘ 𝐵 ) ⊆ I ∧ ran 𝐵 ⊆ dom 𝐵 ) ↔ ( ◡ 𝐵 ⊆ 𝐵 ∧ ( 𝐵 ∘ ◡ 𝐵 ) ⊆ I ) )
10 8 9 sylib ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ( 𝐵 ∘ 𝐵 ) ⊆ I ) → ( ◡ 𝐵 ⊆ 𝐵 ∧ ( 𝐵 ∘ ◡ 𝐵 ) ⊆ I ) )
11 10 simpld ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ( 𝐵 ∘ 𝐵 ) ⊆ I ) → ◡ 𝐵 ⊆ 𝐵 )
12 frel ⊢ ( 𝐵 : 𝑋 ⟶ 𝑋 → Rel 𝐵 )
13 2 12 syl ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ( 𝐵 ∘ 𝐵 ) ⊆ I ) → Rel 𝐵 )
14 dfrel2 ⊢ ( Rel 𝐵 ↔ ◡ ◡ 𝐵 = 𝐵 )
15 13 14 sylib ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ( 𝐵 ∘ 𝐵 ) ⊆ I ) → ◡ ◡ 𝐵 = 𝐵 )
16 cnvss ⊢ ( ◡ 𝐵 ⊆ 𝐵 → ◡ ◡ 𝐵 ⊆ ◡ 𝐵 )
17 11 16 syl ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ( 𝐵 ∘ 𝐵 ) ⊆ I ) → ◡ ◡ 𝐵 ⊆ ◡ 𝐵 )
18 15 17 eqsstrrd ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ( 𝐵 ∘ 𝐵 ) ⊆ I ) → 𝐵 ⊆ ◡ 𝐵 )
19 11 18 eqssd ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ( 𝐵 ∘ 𝐵 ) ⊆ I ) → ◡ 𝐵 = 𝐵 )
20 simpr ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ◡ 𝐵 = 𝐵 ) → ◡ 𝐵 = 𝐵 )
21 20 eqimssd ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ◡ 𝐵 = 𝐵 ) → ◡ 𝐵 ⊆ 𝐵 )
22 simpl ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ◡ 𝐵 = 𝐵 ) → 𝐵 : 𝑋 ⟶ 𝑋 )
23 ffun ⊢ ( 𝐵 : 𝑋 ⟶ 𝑋 → Fun 𝐵 )
24 22 23 syl ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ◡ 𝐵 = 𝐵 ) → Fun 𝐵 )
25 df-fun ⊢ ( Fun 𝐵 ↔ ( Rel 𝐵 ∧ ( 𝐵 ∘ ◡ 𝐵 ) ⊆ I ) )
26 25 simprbi ⊢ ( Fun 𝐵 → ( 𝐵 ∘ ◡ 𝐵 ) ⊆ I )
27 24 26 syl ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ◡ 𝐵 = 𝐵 ) → ( 𝐵 ∘ ◡ 𝐵 ) ⊆ I )
28 21 27 jca ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ◡ 𝐵 = 𝐵 ) → ( ◡ 𝐵 ⊆ 𝐵 ∧ ( 𝐵 ∘ ◡ 𝐵 ) ⊆ I ) )
29 28 9 sylibr ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ◡ 𝐵 = 𝐵 ) → ( ( 𝐵 ∘ 𝐵 ) ⊆ I ∧ ran 𝐵 ⊆ dom 𝐵 ) )
30 29 simpld ⊢ ( ( 𝐵 : 𝑋 ⟶ 𝑋 ∧ ◡ 𝐵 = 𝐵 ) → ( 𝐵 ∘ 𝐵 ) ⊆ I )
31 19 30 impbida ⊢ ( 𝐵 : 𝑋 ⟶ 𝑋 → ( ( 𝐵 ∘ 𝐵 ) ⊆ I ↔ ◡ 𝐵 = 𝐵 ) )