Theorem coi2 6264

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

Assertion

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

Proof of Theorem coi2

Step	Hyp	Ref	Expression
1		dfrel2 6186	. 2 ⊢ (Rel 𝐴 ↔ ◡◡𝐴 = 𝐴)
2		cnvco 5873	. . . 4 ⊢ ◡(◡𝐴 ∘ I ) = (◡ I ∘ ◡◡𝐴)
3		relcnv 6104	. . . . . 6 ⊢ Rel ◡𝐴
4		coi1 6263	. . . . . 6 ⊢ (Rel ◡𝐴 → (◡𝐴 ∘ I ) = ◡𝐴)
5	3, 4	ax-mp 5	. . . . 5 ⊢ (◡𝐴 ∘ I ) = ◡𝐴
6	5	cnveqi 5858	. . . 4 ⊢ ◡(◡𝐴 ∘ I ) = ◡◡𝐴
7	2, 6	eqtr3i 2787	. . 3 ⊢ (◡ I ∘ ◡◡𝐴) = ◡◡𝐴
8		cnvi 5869	. . . 4 ⊢ ◡ I = I
9		coeq2 5842	. . . . 5 ⊢ (◡◡𝐴 = 𝐴 → (◡ I ∘ ◡◡𝐴) = (◡ I ∘ 𝐴))
10		coeq1 5841	. . . . 5 ⊢ (◡ I = I → (◡ I ∘ 𝐴) = ( I ∘ 𝐴))
11	9, 10	sylan9eq 2817	. . . 4 ⊢ ((◡◡𝐴 = 𝐴 ∧ ◡ I = I ) → (◡ I ∘ ◡◡𝐴) = ( I ∘ 𝐴))
12	8, 11	mpan2 704	. . 3 ⊢ (◡◡𝐴 = 𝐴 → (◡ I ∘ ◡◡𝐴) = ( I ∘ 𝐴))
13		id 23	. . 3 ⊢ (◡◡𝐴 = 𝐴 → ◡◡𝐴 = 𝐴)
14	7, 12, 13	3eqtr3a 2821	. 2 ⊢ (◡◡𝐴 = 𝐴 → ( I ∘ 𝐴) = 𝐴)
15	1, 14	sylbi 220	1 ⊢ (Rel 𝐴 → ( I ∘ 𝐴) = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   I cid 5553  ^◡ccnv 5658   ∘ ccom 5663  Rel wrel 5664

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402

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 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668

This theorem is used by:  relcoi2  6279  funi  6569  fcoi2  6754