Theorem relcoi1 4792

Description: Composition with the identity relation restricted to a relation's field. (Contributed by FL, 8-May-2011.)

Assertion

Ref	Expression
relcoi1	|- ( Rel R -> ( R o. ( _I |` U. U. R)) = R)

Proof of Theorem relcoi1

Step	Hyp	Ref	Expression
1		relfld 4789	. . 3 |- ( Rel R -> U. U. R = ( dom R u. ran R))
2		resundi 4568	. . . . 5 |- ( _I |` ( dom R u. ran R)) = (( _I |` dom R) u. ( _I |` ran R))
3		coeq2 4437	. . . . 5 |- (( _I |` ( dom R u. ran R)) = (( _I |` dom R) u. ( _I |` ran R)) -> ( R o. ( _I |` ( dom R u. ran R))) = ( R o. (( _I |` dom R) u. ( _I |` ran R))))
4		coundi 4765	. . . . . . 7 |- ( R o. (( _I |` dom R) u. ( _I |` ran R))) = (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R)))
5		resco 4768	. . . . . . . 8 |- (( R o. _I ) |` dom R) = ( R o. ( _I |` dom R))
6		coi1 4779	. . . . . . . . 9 |- ( Rel R -> ( R o. _I ) = R)
7		reseq1 4549	. . . . . . . . . 10 |- (( R o. _I ) = R -> (( R o. _I ) |` dom R) = ( R |` dom R))
8		resdm 4592	. . . . . . . . . . 11 |- ( Rel R -> ( R |` dom R) = R)
9		eqtr 2054	. . . . . . . . . . . . . 14 |- (((( R o. _I ) |` dom R) = ( R |` dom R) /\ ( R |` dom R) = R) -> (( R o. _I ) |` dom R) = R)
10		eqtr 2054	. . . . . . . . . . . . . . . . . 18 |- ((( R o. ( _I |` dom R)) = (( R o. _I ) |` dom R) /\ (( R o. _I ) |` dom R) = R) -> ( R o. ( _I |` dom R)) = R)
11		resco 4768	. . . . . . . . . . . . . . . . . . 19 |- (( R o. _I ) |` ran R) = ( R o. ( _I |` ran R))
12		uneq1 3084	. . . . . . . . . . . . . . . . . . 19 |- (( R o. ( _I |` dom R)) = R -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R u. ( R o. ( _I |` ran R))))
13		reseq1 4549	. . . . . . . . . . . . . . . . . . . . . 22 |- (( R o. _I ) = R -> (( R o. _I ) |` ran R) = ( R |` ran R))
14		eqtr 2054	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((( R o. ( _I |` ran R)) = (( R o. _I ) |` ran R) /\ (( R o. _I ) |` ran R) = ( R |` ran R)) -> ( R o. ( _I |` ran R)) = ( R |` ran R))
15	14	uneq2d 3091	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((( R o. ( _I |` ran R)) = (( R o. _I ) |` ran R) /\ (( R o. _I ) |` ran R) = ( R |` ran R)) -> ( R u. ( R o. ( _I |` ran R))) = ( R u. ( R |` ran R)))
16		eqtr 2054	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R u. ( R o. ( _I |` ran R))) /\ ( R u. ( R o. ( _I |` ran R))) = ( R u. ( R |` ran R))) -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R u. ( R |` ran R)))
17		resss 4578	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( R |` ran R) C_ R
18		ssequn2 3110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (( R |` ran R) C_ R <-> ( R u. ( R |` ran R)) = R)
19	17, 18	mpbi 133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( R u. ( R |` ran R)) = R
20	6, 19	syl6reqr 2088	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( Rel R -> ( R u. ( R |` ran R)) = ( R o. _I ))
21		eqeq1 2043	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R u. ( R |` ran R)) -> ((( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I ) <-> ( R u. ( R |` ran R)) = ( R o. _I )))
22	20, 21	syl5ibr 145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R u. ( R |` ran R)) -> ( Rel R -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I )))
23	16, 22	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R u. ( R o. ( _I |` ran R))) /\ ( R u. ( R o. ( _I |` ran R))) = ( R u. ( R |` ran R))) -> ( Rel R -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I )))
24	23	ex 108	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R u. ( R o. ( _I |` ran R))) -> (( R u. ( R o. ( _I |` ran R))) = ( R u. ( R |` ran R)) -> ( Rel R -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I ))))
25	24	com3l 75	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (( R u. ( R o. ( _I |` ran R))) = ( R u. ( R |` ran R)) -> ( Rel R -> ((( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R u. ( R o. ( _I |` ran R))) -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I ))))
26	15, 25	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((( R o. ( _I |` ran R)) = (( R o. _I ) |` ran R) /\ (( R o. _I ) |` ran R) = ( R |` ran R)) -> ( Rel R -> ((( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R u. ( R o. ( _I |` ran R))) -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I ))))
27	26	ex 108	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (( R o. ( _I |` ran R)) = (( R o. _I ) |` ran R) -> ((( R o. _I ) |` ran R) = ( R |` ran R) -> ( Rel R -> ((( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R u. ( R o. ( _I |` ran R))) -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I )))))
28	27	eqcoms 2040	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((( R o. _I ) |` ran R) = ( R o. ( _I |` ran R)) -> ((( R o. _I ) |` ran R) = ( R |` ran R) -> ( Rel R -> ((( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R u. ( R o. ( _I |` ran R))) -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I )))))
29	28	com3l 75	. . . . . . . . . . . . . . . . . . . . . 22 |- ((( R o. _I ) |` ran R) = ( R |` ran R) -> ( Rel R -> ((( R o. _I ) |` ran R) = ( R o. ( _I |` ran R)) -> ((( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R u. ( R o. ( _I |` ran R))) -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I )))))
30	13, 29	syl 14	. . . . . . . . . . . . . . . . . . . . 21 |- (( R o. _I ) = R -> ( Rel R -> ((( R o. _I ) |` ran R) = ( R o. ( _I |` ran R)) -> ((( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R u. ( R o. ( _I |` ran R))) -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I )))))
31	6, 30	mpcom 32	. . . . . . . . . . . . . . . . . . . 20 |- ( Rel R -> ((( R o. _I ) |` ran R) = ( R o. ( _I |` ran R)) -> ((( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R u. ( R o. ( _I |` ran R))) -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I ))))
32	31	com3l 75	. . . . . . . . . . . . . . . . . . 19 |- ((( R o. _I ) |` ran R) = ( R o. ( _I |` ran R)) -> ((( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R u. ( R o. ( _I |` ran R))) -> ( Rel R -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I ))))
33	11, 12, 32	mpsyl 59	. . . . . . . . . . . . . . . . . 18 |- (( R o. ( _I |` dom R)) = R -> ( Rel R -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I )))
34	10, 33	syl 14	. . . . . . . . . . . . . . . . 17 |- ((( R o. ( _I |` dom R)) = (( R o. _I ) |` dom R) /\ (( R o. _I ) |` dom R) = R) -> ( Rel R -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I )))
35	34	ex 108	. . . . . . . . . . . . . . . 16 |- (( R o. ( _I |` dom R)) = (( R o. _I ) |` dom R) -> ((( R o. _I ) |` dom R) = R -> ( Rel R -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I ))))
36	35	eqcoms 2040	. . . . . . . . . . . . . . 15 |- ((( R o. _I ) |` dom R) = ( R o. ( _I |` dom R)) -> ((( R o. _I ) |` dom R) = R -> ( Rel R -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I ))))
37	36	com3l 75	. . . . . . . . . . . . . 14 |- ((( R o. _I ) |` dom R) = R -> ( Rel R -> ((( R o. _I ) |` dom R) = ( R o. ( _I |` dom R)) -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I ))))
38	9, 37	syl 14	. . . . . . . . . . . . 13 |- (((( R o. _I ) |` dom R) = ( R |` dom R) /\ ( R |` dom R) = R) -> ( Rel R -> ((( R o. _I ) |` dom R) = ( R o. ( _I |` dom R)) -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I ))))
39	38	ex 108	. . . . . . . . . . . 12 |- ((( R o. _I ) |` dom R) = ( R |` dom R) -> (( R |` dom R) = R -> ( Rel R -> ((( R o. _I ) |` dom R) = ( R o. ( _I |` dom R)) -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I )))))
40	39	com3l 75	. . . . . . . . . . 11 |- (( R |` dom R) = R -> ( Rel R -> ((( R o. _I ) |` dom R) = ( R |` dom R) -> ((( R o. _I ) |` dom R) = ( R o. ( _I |` dom R)) -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I )))))
41	8, 40	mpcom 32	. . . . . . . . . 10 |- ( Rel R -> ((( R o. _I ) |` dom R) = ( R |` dom R) -> ((( R o. _I ) |` dom R) = ( R o. ( _I |` dom R)) -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I ))))
42	7, 41	syl5com 26	. . . . . . . . 9 |- (( R o. _I ) = R -> ( Rel R -> ((( R o. _I ) |` dom R) = ( R o. ( _I |` dom R)) -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I ))))
43	6, 42	mpcom 32	. . . . . . . 8 |- ( Rel R -> ((( R o. _I ) |` dom R) = ( R o. ( _I |` dom R)) -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I )))
44	5, 43	mpi 15	. . . . . . 7 |- ( Rel R -> (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R))) = ( R o. _I ))
45	4, 44	syl5eq 2081	. . . . . 6 |- ( Rel R -> ( R o. (( _I |` dom R) u. ( _I |` ran R))) = ( R o. _I ))
46		eqeq1 2043	. . . . . 6 |- (( R o. ( _I |` ( dom R u. ran R))) = ( R o. (( _I |` dom R) u. ( _I |` ran R))) -> (( R o. ( _I |` ( dom R u. ran R))) = ( R o. _I ) <-> ( R o. (( _I |` dom R) u. ( _I |` ran R))) = ( R o. _I )))
47	45, 46	syl5ibr 145	. . . . 5 |- (( R o. ( _I |` ( dom R u. ran R))) = ( R o. (( _I |` dom R) u. ( _I |` ran R))) -> ( Rel R -> ( R o. ( _I |` ( dom R u. ran R))) = ( R o. _I )))
48	2, 3, 47	mp2b 8	. . . 4 |- ( Rel R -> ( R o. ( _I |` ( dom R u. ran R))) = ( R o. _I ))
49		reseq2 4550	. . . . . 6 |- ( U. U. R = ( dom R u. ran R) -> ( _I |` U. U. R) = ( _I |` ( dom R u. ran R)))
50	49	coeq2d 4441	. . . . 5 |- ( U. U. R = ( dom R u. ran R) -> ( R o. ( _I |` U. U. R)) = ( R o. ( _I |` ( dom R u. ran R))))
51	50	eqeq1d 2045	. . . 4 |- ( U. U. R = ( dom R u. ran R) -> (( R o. ( _I |` U. U. R)) = ( R o. _I ) <-> ( R o. ( _I |` ( dom R u. ran R))) = ( R o. _I )))
52	48, 51	syl5ibr 145	. . 3 |- ( U. U. R = ( dom R u. ran R) -> ( Rel R -> ( R o. ( _I |` U. U. R)) = ( R o. _I )))
53	1, 52	mpcom 32	. 2 |- ( Rel R -> ( R o. ( _I |` U. U. R)) = ( R o. _I ))
54	53, 6	eqtrd 2069	1 |- ( Rel R -> ( R o. ( _I |` U. U. R)) = R)

Syntax hints:   -> wi 4   /\ wa 97   = wceq 1242   u. cun 2909   C_ wss 2911   U.cuni 3571   _I cid 4016   dom cdm 4288   ran crn 4289   |` cres 4290   o. ccom 4292   Rel wrel 4293

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300

This theorem is referenced by: (None)