Theorem idresdmsscocnv1

Description: A class postcomposed with its converse includes the identity relation restricted to its domain. (Contributed by BJ, 25-Oct-2026)

	Ref	Expression
Assertion	idresdmsscocnv1	⊢ ( I ↾ dom 𝐴 ) ⊆ ( ◡ 𝐴 ∘ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		relres	⊢ Rel ( I ↾ dom 𝐴 )
2		vex	⊢ 𝑦 ∈ V
3	2	brresi	⊢ ( 𝑥 ( I ↾ dom 𝐴 ) 𝑦 ↔ ( 𝑥 ∈ dom 𝐴 ∧ 𝑥 I 𝑦 ) )
4		vex	⊢ 𝑥 ∈ V
5	4	eldm	⊢ ( 𝑥 ∈ dom 𝐴 ↔ ∃ 𝑧 𝑥 𝐴 𝑧 )
6		vex	⊢ 𝑧 ∈ V
7	6 4	brcnv	⊢ ( 𝑧 ◡ 𝐴 𝑥 ↔ 𝑥 𝐴 𝑧 )
8	4 6 4	brcoi	⊢ ( ( 𝑥 𝐴 𝑧 ∧ 𝑧 ◡ 𝐴 𝑥 ) → 𝑥 ( ◡ 𝐴 ∘ 𝐴 ) 𝑥 )
9	7 8	sylan2br	⊢ ( ( 𝑥 𝐴 𝑧 ∧ 𝑥 𝐴 𝑧 ) → 𝑥 ( ◡ 𝐴 ∘ 𝐴 ) 𝑥 )
10	9	anidms	⊢ ( 𝑥 𝐴 𝑧 → 𝑥 ( ◡ 𝐴 ∘ 𝐴 ) 𝑥 )
11	10	exlimiv	⊢ ( ∃ 𝑧 𝑥 𝐴 𝑧 → 𝑥 ( ◡ 𝐴 ∘ 𝐴 ) 𝑥 )
12	5 11	sylbi	⊢ ( 𝑥 ∈ dom 𝐴 → 𝑥 ( ◡ 𝐴 ∘ 𝐴 ) 𝑥 )
13	2	ideq	⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 )
14		breq2	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ( ◡ 𝐴 ∘ 𝐴 ) 𝑥 ↔ 𝑥 ( ◡ 𝐴 ∘ 𝐴 ) 𝑦 ) )
15	13 14	sylbi	⊢ ( 𝑥 I 𝑦 → ( 𝑥 ( ◡ 𝐴 ∘ 𝐴 ) 𝑥 ↔ 𝑥 ( ◡ 𝐴 ∘ 𝐴 ) 𝑦 ) )
16	15	biimpac	⊢ ( ( 𝑥 ( ◡ 𝐴 ∘ 𝐴 ) 𝑥 ∧ 𝑥 I 𝑦 ) → 𝑥 ( ◡ 𝐴 ∘ 𝐴 ) 𝑦 )
17	12 16	sylan	⊢ ( ( 𝑥 ∈ dom 𝐴 ∧ 𝑥 I 𝑦 ) → 𝑥 ( ◡ 𝐴 ∘ 𝐴 ) 𝑦 )
18	3 17	sylbi	⊢ ( 𝑥 ( I ↾ dom 𝐴 ) 𝑦 → 𝑥 ( ◡ 𝐴 ∘ 𝐴 ) 𝑦 )
19		df-br	⊢ ( 𝑥 ( I ↾ dom 𝐴 ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ dom 𝐴 ) )
20		df-br	⊢ ( 𝑥 ( ◡ 𝐴 ∘ 𝐴 ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝐴 ∘ 𝐴 ) )
21	18 19 20	3imtr3i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ dom 𝐴 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝐴 ∘ 𝐴 ) )
22	1 21	relssi	⊢ ( I ↾ dom 𝐴 ) ⊆ ( ◡ 𝐴 ∘ 𝐴 )