Theorem coi2

Description: Composition with the identity relation. Part of Theorem 3.7(i) of Monk1 p. 36. (Contributed by NM, 22-Apr-2004)

	Ref	Expression
Assertion	coi2	⊢ ( Rel 𝐴 → ( I ∘ 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dfrel2	⊢ ( Rel 𝐴 ↔ ◡ ◡ 𝐴 = 𝐴 )
2		cnvco	⊢ ◡ ( ◡ 𝐴 ∘ I ) = ( ◡ I ∘ ◡ ◡ 𝐴 )
3		relcnv	⊢ Rel ◡ 𝐴
4		coi1	⊢ ( Rel ◡ 𝐴 → ( ◡ 𝐴 ∘ I ) = ◡ 𝐴 )
5	3 4	ax-mp	⊢ ( ◡ 𝐴 ∘ I ) = ◡ 𝐴
6	5	cnveqi	⊢ ◡ ( ◡ 𝐴 ∘ I ) = ◡ ◡ 𝐴
7	2 6	eqtr3i	⊢ ( ◡ I ∘ ◡ ◡ 𝐴 ) = ◡ ◡ 𝐴
8		cnvi	⊢ ◡ I = I
9		coeq2	⊢ ( ◡ ◡ 𝐴 = 𝐴 → ( ◡ I ∘ ◡ ◡ 𝐴 ) = ( ◡ I ∘ 𝐴 ) )
10		coeq1	⊢ ( ◡ I = I → ( ◡ I ∘ 𝐴 ) = ( I ∘ 𝐴 ) )
11	9 10	sylan9eq	⊢ ( ( ◡ ◡ 𝐴 = 𝐴 ∧ ◡ I = I ) → ( ◡ I ∘ ◡ ◡ 𝐴 ) = ( I ∘ 𝐴 ) )
12	8 11	mpan2	⊢ ( ◡ ◡ 𝐴 = 𝐴 → ( ◡ I ∘ ◡ ◡ 𝐴 ) = ( I ∘ 𝐴 ) )
13		id	⊢ ( ◡ ◡ 𝐴 = 𝐴 → ◡ ◡ 𝐴 = 𝐴 )
14	7 12 13	3eqtr3a	⊢ ( ◡ ◡ 𝐴 = 𝐴 → ( I ∘ 𝐴 ) = 𝐴 )
15	1 14	sylbi	⊢ ( Rel 𝐴 → ( I ∘ 𝐴 ) = 𝐴 )