Theorem coi2 4414

Description: Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36.

Assertion

Ref	Expression
coi2	|- (Rel A -> ( _I o. A) = A)

Proof of Theorem coi2

Step	Hyp	Ref	Expression
1		dfrel2 4358	. . . 4 |- (Rel A <-> `'`'A = A)
2		cnvi 4320	. . . . 5 |- `' _I = _I
3		coeq2 4124	. . . . . 6 |- (`'`'A = A -> (`' _I o. `'`'A) = (`' _I o. A))
4		coeq1 4123	. . . . . 6 |- (`' _I = _I -> (`' _I o. A) = ( _I o. A))
5	3, 4	sylan9eq 1948	. . . . 5 |- ((`'`'A = A /\ `' _I = _I ) -> (`' _I o. `'`'A) = ( _I o. A))
6	2, 5	mpan2 760	. . . 4 |- (`'`'A = A -> (`' _I o. `'`'A) = ( _I o. A))
7	1, 6	sylbi 216	. . 3 |- (Rel A -> (`' _I o. `'`'A) = ( _I o. A))
8		cnvco 4145	. . . 4 |- `'(`'A o. _I ) = (`' _I o. `'`'A)
9		relcnv 4301	. . . . . 6 |- Rel `'A
10		coi1 4413	. . . . . 6 |- (Rel `'A -> (`'A o. _I ) = `'A)
11	9, 10	ax-mp 7	. . . . 5 |- (`'A o. _I ) = `'A
12	11	cnveqi 4136	. . . 4 |- `'(`'A o. _I ) = `'`'A
13	8, 12	eqtr3i 1910	. . 3 |- (`' _I o. `'`'A) = `'`'A
14	7, 13	syl5reqr 1943	. 2 |- (Rel A -> ( _I o. A) = `'`'A)
15	1	biimpi 168	. 2 |- (Rel A -> `'`'A = A)
16	14, 15	eqtrd 1925	1 |- (Rel A -> ( _I o. A) = A)

Syntax hints:   -> wi 3   = wceq 1298   _I cid 3582  `'ccnv 3985   o. ccom 3990  Rel wrel 3991

This theorem is referenced by:  funi 4452  fcoi2 4586  cmprelid1 14445  dfps2 14634

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003

Copyright terms: Public domain