Theorem relcoi1 4772

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 4769	. . 3 |- ( Rel R -> U. U. R = ( dom R u. ran R))
2		resundi 4548	. . . . 5 |- ( _I |` ( dom R u. ran R)) = (( _I |` dom R) u. ( _I |` ran R))
3		coeq2 4417	. . . . 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 4745	. . . . . . 7 |- ( R o. (( _I |` dom R) u. ( _I |` ran R))) = (( R o. ( _I |` dom R)) u. ( R o. ( _I |` ran R)))
5		resco 4748	. . . . . . . 8 |- (( R o. _I ) |` dom R) = ( R o. ( _I |` dom R))
6		coi1 4759	. . . . . . . . 9 |- ( Rel R -> ( R o. _I ) = R)
7		reseq1 4529	. . . . . . . . . 10 |- (( R o. _I ) = R -> (( R o. _I ) |` dom R) = ( R |` dom R))
8		resdm 4572	. . . . . . . . . . 11 |- ( Rel R -> ( R |` dom R) = R)
9		eqtr 2035	. . . . . . . . . . . . . 14 |- (((( R o. _I ) |` dom R) = ( R |` dom R) /\ ( R |` dom R) = R) -> (( R o. _I ) |` dom R) = R)
10		eqtr 2035	. . . . . . . . . . . . . . . . . 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 4748	. . . . . . . . . . . . . . . . . . 19 |- (( R o. _I ) |` ran R) = ( R o. ( _I |` ran R))
12		uneq1 3063	. . . . . . . . . . . . . . . . . . 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 4529	. . . . . . . . . . . . . . . . . . . . . 22 |- (( R o. _I ) = R -> (( R o. _I ) |` ran R) = ( R |` ran R))
14		eqtr 2035	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 3070	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4558	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( R |` ran R) C_ R
18		ssequn2 3089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( Rel R -> ( R u. ( R |` ran R)) = ( R o. _I ))
21		eqeq1 2024	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2021	. . . . . . . . . . . . . . . . . . . . . . 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 2021	. . . . . . . . . . . . . . 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 2062	. . . . . 6 |- ( Rel R -> ( R o. (( _I |` dom R) u. ( _I |` ran R))) = ( R o. _I ))
46		eqeq1 2024	. . . . . 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 4530	. . . . . 6 |- ( U. U. R = ( dom R u. ran R) -> ( _I |` U. U. R) = ( _I |` ( dom R u. ran R)))
50	49	coeq2d 4421	. . . . 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 2026	. . . 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 2050	1 |- ( Rel R -> ( R o. ( _I |` U. U. R)) = R)

Syntax hints:   -> wi 4   /\ wa 97   = wceq 1226   u. cun 2888   C_ wss 2890   U.cuni 3550   _I cid 3995   dom cdm 4268   ran crn 4269   |` cres 4270   o. ccom 4272   Rel wrel 4273

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 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914

This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-v 2533  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-br 3735  df-opab 3789  df-id 4000  df-xp 4274  df-rel 4275  df-cnv 4276  df-co 4277  df-dm 4278  df-rn 4279  df-res 4280

This theorem is referenced by: (None)