Theorem coi1

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	coi1	$$⊢\mathrm{Rel}A\to A\circ \mathrm{I}=A$$

Proof

Step	Hyp	Ref	Expression
1		relco	$$⊢\mathrm{Rel}\left(A\circ \mathrm{I}\right)$$
2		vex	$$⊢x\in \mathrm{V}$$
3		vex	$$⊢y\in \mathrm{V}$$
4	2 3	opelco	$$⊢⟨x,y⟩\in \left(A\circ \mathrm{I}\right)\leftrightarrow \exists z\left(x\mathrm{I}z\wedge zAy\right)$$
5		vex	$$⊢z\in \mathrm{V}$$
6	5	ideq	$$⊢x\mathrm{I}z\leftrightarrow x=z$$
7		equcom	$$⊢x=z\leftrightarrow z=x$$
8	6 7	bitri	$$⊢x\mathrm{I}z\leftrightarrow z=x$$
9	8	anbi1i	$$⊢\left(x\mathrm{I}z\wedge zAy\right)\leftrightarrow \left(z=x\wedge zAy\right)$$
10	9	exbii	$$⊢\exists z\left(x\mathrm{I}z\wedge zAy\right)\leftrightarrow \exists z\left(z=x\wedge zAy\right)$$
11		breq1	$$⊢z=x\to \left(zAy\leftrightarrow xAy\right)$$
12	11	equsexvw	$$⊢\exists z\left(z=x\wedge zAy\right)\leftrightarrow xAy$$
13	10 12	bitri	$$⊢\exists z\left(x\mathrm{I}z\wedge zAy\right)\leftrightarrow xAy$$
14	4 13	bitri	$$⊢⟨x,y⟩\in \left(A\circ \mathrm{I}\right)\leftrightarrow xAy$$
15		df-br	$$⊢xAy\leftrightarrow ⟨x,y⟩\in A$$
16	14 15	bitri	$$⊢⟨x,y⟩\in \left(A\circ \mathrm{I}\right)\leftrightarrow ⟨x,y⟩\in A$$
17	16	eqrelriv	$$⊢\left(\mathrm{Rel}\left(A\circ \mathrm{I}\right)\wedge \mathrm{Rel}A\right)\to A\circ \mathrm{I}=A$$
18	1 17	mpan	$$⊢\mathrm{Rel}A\to A\circ \mathrm{I}=A$$