Theorem nvo2 38222

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 7318.

Assertion

Ref	Expression
nvo2	⊢ (𝐵:𝑋⟶𝑋 → ((𝐵 ∘ 𝐵) ⊆ I ↔ ◡𝐵 = 𝐵))

Proof of Theorem nvo2

Step	Hyp	Ref	Expression
1		simpr 490	. . . . . 6 ⊢ ((𝐵:𝑋⟶𝑋 ∧ (𝐵 ∘ 𝐵) ⊆ I ) → (𝐵 ∘ 𝐵) ⊆ I )
2		simpl 488	. . . . . . . 8 ⊢ ((𝐵:𝑋⟶𝑋 ∧ (𝐵 ∘ 𝐵) ⊆ I ) → 𝐵:𝑋⟶𝑋)
3		frn 6745	. . . . . . . 8 ⊢ (𝐵:𝑋⟶𝑋 → ran 𝐵 ⊆ 𝑋)
4	2, 3	syl 18	. . . . . . 7 ⊢ ((𝐵:𝑋⟶𝑋 ∧ (𝐵 ∘ 𝐵) ⊆ I ) → ran 𝐵 ⊆ 𝑋)
5		fdm 6747	. . . . . . . 8 ⊢ (𝐵:𝑋⟶𝑋 → dom 𝐵 = 𝑋)
6	2, 5	syl 18	. . . . . . 7 ⊢ ((𝐵:𝑋⟶𝑋 ∧ (𝐵 ∘ 𝐵) ⊆ I ) → dom 𝐵 = 𝑋)
7	4, 6	sseqtrrd 3950	. . . . . 6 ⊢ ((𝐵:𝑋⟶𝑋 ∧ (𝐵 ∘ 𝐵) ⊆ I ) → ran 𝐵 ⊆ dom 𝐵)
8	1, 7	jca 521	. . . . 5 ⊢ ((𝐵:𝑋⟶𝑋 ∧ (𝐵 ∘ 𝐵) ⊆ I ) → ((𝐵 ∘ 𝐵) ⊆ I ∧ ran 𝐵 ⊆ dom 𝐵))
9		cossidcnvss 38216	. . . . 5 ⊢ (((𝐵 ∘ 𝐵) ⊆ I ∧ ran 𝐵 ⊆ dom 𝐵) ↔ (◡𝐵 ⊆ 𝐵 ∧ (𝐵 ∘ ◡𝐵) ⊆ I ))
10	8, 9	sylib 221	. . . 4 ⊢ ((𝐵:𝑋⟶𝑋 ∧ (𝐵 ∘ 𝐵) ⊆ I ) → (◡𝐵 ⊆ 𝐵 ∧ (𝐵 ∘ ◡𝐵) ⊆ I ))
11	10	simpld 500	. . 3 ⊢ ((𝐵:𝑋⟶𝑋 ∧ (𝐵 ∘ 𝐵) ⊆ I ) → ◡𝐵 ⊆ 𝐵)
12		frel 6743	. . . . . 6 ⊢ (𝐵:𝑋⟶𝑋 → Rel 𝐵)
13	2, 12	syl 18	. . . . 5 ⊢ ((𝐵:𝑋⟶𝑋 ∧ (𝐵 ∘ 𝐵) ⊆ I ) → Rel 𝐵)
14		dfrel2 6197	. . . . 5 ⊢ (Rel 𝐵 ↔ ◡◡𝐵 = 𝐵)
15	13, 14	sylib 221	. . . 4 ⊢ ((𝐵:𝑋⟶𝑋 ∧ (𝐵 ∘ 𝐵) ⊆ I ) → ◡◡𝐵 = 𝐵)
16		cnvss 5860	. . . . 5 ⊢ (◡𝐵 ⊆ 𝐵 → ◡◡𝐵 ⊆ ◡𝐵)
17	11, 16	syl 18	. . . 4 ⊢ ((𝐵:𝑋⟶𝑋 ∧ (𝐵 ∘ 𝐵) ⊆ I ) → ◡◡𝐵 ⊆ ◡𝐵)
18	15, 17	eqsstrrd 3948	. . 3 ⊢ ((𝐵:𝑋⟶𝑋 ∧ (𝐵 ∘ 𝐵) ⊆ I ) → 𝐵 ⊆ ◡𝐵)
19	11, 18	eqssd 3930	. 2 ⊢ ((𝐵:𝑋⟶𝑋 ∧ (𝐵 ∘ 𝐵) ⊆ I ) → ◡𝐵 = 𝐵)
20		simpr 490	. . . . . 6 ⊢ ((𝐵:𝑋⟶𝑋 ∧ ◡𝐵 = 𝐵) → ◡𝐵 = 𝐵)
21	20	eqimssd 3969	. . . . 5 ⊢ ((𝐵:𝑋⟶𝑋 ∧ ◡𝐵 = 𝐵) → ◡𝐵 ⊆ 𝐵)
22		simpl 488	. . . . . . 7 ⊢ ((𝐵:𝑋⟶𝑋 ∧ ◡𝐵 = 𝐵) → 𝐵:𝑋⟶𝑋)
23		ffun 6740	. . . . . . 7 ⊢ (𝐵:𝑋⟶𝑋 → Fun 𝐵)
24	22, 23	syl 18	. . . . . 6 ⊢ ((𝐵:𝑋⟶𝑋 ∧ ◡𝐵 = 𝐵) → Fun 𝐵)
25		df-fun 6566	. . . . . . 7 ⊢ (Fun 𝐵 ↔ (Rel 𝐵 ∧ (𝐵 ∘ ◡𝐵) ⊆ I ))
26	25	simprbi 503	. . . . . 6 ⊢ (Fun 𝐵 → (𝐵 ∘ ◡𝐵) ⊆ I )
27	24, 26	syl 18	. . . . 5 ⊢ ((𝐵:𝑋⟶𝑋 ∧ ◡𝐵 = 𝐵) → (𝐵 ∘ ◡𝐵) ⊆ I )
28	21, 27	jca 521	. . . 4 ⊢ ((𝐵:𝑋⟶𝑋 ∧ ◡𝐵 = 𝐵) → (◡𝐵 ⊆ 𝐵 ∧ (𝐵 ∘ ◡𝐵) ⊆ I ))
29	28, 9	sylibr 237	. . 3 ⊢ ((𝐵:𝑋⟶𝑋 ∧ ◡𝐵 = 𝐵) → ((𝐵 ∘ 𝐵) ⊆ I ∧ ran 𝐵 ⊆ dom 𝐵))
30	29	simpld 500	. 2 ⊢ ((𝐵:𝑋⟶𝑋 ∧ ◡𝐵 = 𝐵) → (𝐵 ∘ 𝐵) ⊆ I )
31	19, 30	impbida 813	1 ⊢ (𝐵:𝑋⟶𝑋 → ((𝐵 ∘ 𝐵) ⊆ I ↔ ◡𝐵 = 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ⊆ wss 3900   I cid 5550  ^◡ccnv 5655  dom cdm 5656  ran crn 5657   ∘ ccom 5660  Rel wrel 5661  Fun wfun 6558  ⟶wf 6560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pr 5396

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5172  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-fun 6566  df-fn 6567  df-f 6568

This theorem is used by:  nvo3  38223