Theorem trclexi

Description: The transitive closure of a set exists. (Contributed by RP, 27-Oct-2020)

	Ref	Expression
Hypothesis	trclexi.1	$$⊢A\in V$$
Assertion	trclexi	$$⊢\bigcap \left\{x|\left(A\subseteq x\wedge x\circ x\subseteq x\right)\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		trclexi.1	$$⊢A\in V$$
2		ssun1	$$⊢A\subseteq A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)$$
3		coundir	$$⊢\left(A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\circ \left(A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)=\left(A\circ \left(A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\right)\cup \left(\left(\mathrm{dom}A\times \mathrm{ran}A\right)\circ \left(A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\right)$$
4		coundi	$$⊢A\circ \left(A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)=\left(A\circ A\right)\cup \left(A\circ \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)$$
5		cossxp	$$⊢A\circ A\subseteq \mathrm{dom}A\times \mathrm{ran}A$$
6		cossxp	$$⊢A\circ \left(\mathrm{dom}A\times \mathrm{ran}A\right)\subseteq \mathrm{dom}\left(\mathrm{dom}A\times \mathrm{ran}A\right)\times \mathrm{ran}A$$
7		dmxpss	$$⊢\mathrm{dom}\left(\mathrm{dom}A\times \mathrm{ran}A\right)\subseteq \mathrm{dom}A$$
8		xpss1	$$⊢\mathrm{dom}\left(\mathrm{dom}A\times \mathrm{ran}A\right)\subseteq \mathrm{dom}A\to \mathrm{dom}\left(\mathrm{dom}A\times \mathrm{ran}A\right)\times \mathrm{ran}A\subseteq \mathrm{dom}A\times \mathrm{ran}A$$
9	7 8	ax-mp	$$⊢\mathrm{dom}\left(\mathrm{dom}A\times \mathrm{ran}A\right)\times \mathrm{ran}A\subseteq \mathrm{dom}A\times \mathrm{ran}A$$
10	6 9	sstri	$$⊢A\circ \left(\mathrm{dom}A\times \mathrm{ran}A\right)\subseteq \mathrm{dom}A\times \mathrm{ran}A$$
11	5 10	unssi	$$⊢\left(A\circ A\right)\cup \left(A\circ \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\subseteq \mathrm{dom}A\times \mathrm{ran}A$$
12	4 11	eqsstri	$$⊢A\circ \left(A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\subseteq \mathrm{dom}A\times \mathrm{ran}A$$
13		coundi	$$⊢\left(\mathrm{dom}A\times \mathrm{ran}A\right)\circ \left(A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)=\left(\left(\mathrm{dom}A\times \mathrm{ran}A\right)\circ A\right)\cup \left(\left(\mathrm{dom}A\times \mathrm{ran}A\right)\circ \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)$$
14		cossxp	$$⊢\left(\mathrm{dom}A\times \mathrm{ran}A\right)\circ A\subseteq \mathrm{dom}A\times \mathrm{ran}\left(\mathrm{dom}A\times \mathrm{ran}A\right)$$
15		rnxpss	$$⊢\mathrm{ran}\left(\mathrm{dom}A\times \mathrm{ran}A\right)\subseteq \mathrm{ran}A$$
16		xpss2	$$⊢\mathrm{ran}\left(\mathrm{dom}A\times \mathrm{ran}A\right)\subseteq \mathrm{ran}A\to \mathrm{dom}A\times \mathrm{ran}\left(\mathrm{dom}A\times \mathrm{ran}A\right)\subseteq \mathrm{dom}A\times \mathrm{ran}A$$
17	15 16	ax-mp	$$⊢\mathrm{dom}A\times \mathrm{ran}\left(\mathrm{dom}A\times \mathrm{ran}A\right)\subseteq \mathrm{dom}A\times \mathrm{ran}A$$
18	14 17	sstri	$$⊢\left(\mathrm{dom}A\times \mathrm{ran}A\right)\circ A\subseteq \mathrm{dom}A\times \mathrm{ran}A$$
19		xptrrel	$$⊢\left(\mathrm{dom}A\times \mathrm{ran}A\right)\circ \left(\mathrm{dom}A\times \mathrm{ran}A\right)\subseteq \mathrm{dom}A\times \mathrm{ran}A$$
20	18 19	unssi	$$⊢\left(\left(\mathrm{dom}A\times \mathrm{ran}A\right)\circ A\right)\cup \left(\left(\mathrm{dom}A\times \mathrm{ran}A\right)\circ \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\subseteq \mathrm{dom}A\times \mathrm{ran}A$$
21	13 20	eqsstri	$$⊢\left(\mathrm{dom}A\times \mathrm{ran}A\right)\circ \left(A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\subseteq \mathrm{dom}A\times \mathrm{ran}A$$
22	12 21	unssi	$$⊢\left(A\circ \left(A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\right)\cup \left(\left(\mathrm{dom}A\times \mathrm{ran}A\right)\circ \left(A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\right)\subseteq \mathrm{dom}A\times \mathrm{ran}A$$
23	3 22	eqsstri	$$⊢\left(A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\circ \left(A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\subseteq \mathrm{dom}A\times \mathrm{ran}A$$
24		ssun2	$$⊢\mathrm{dom}A\times \mathrm{ran}A\subseteq A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)$$
25	23 24	sstri	$$⊢\left(A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\circ \left(A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\subseteq A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)$$
26	1	elexi	$$⊢A\in \mathrm{V}$$
27	26	dmex	$$⊢\mathrm{dom}A\in \mathrm{V}$$
28	26	rnex	$$⊢\mathrm{ran}A\in \mathrm{V}$$
29	27 28	xpex	$$⊢\mathrm{dom}A\times \mathrm{ran}A\in \mathrm{V}$$
30	26 29	unex	$$⊢A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\in \mathrm{V}$$
31		trcleq2lem	$$⊢x=A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\to \left(\left(A\subseteq x\wedge x\circ x\subseteq x\right)\leftrightarrow \left(A\subseteq A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\wedge \left(A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\circ \left(A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\subseteq A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\right)$$
32	30 31	spcev	$$⊢\left(A\subseteq A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\wedge \left(A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\circ \left(A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\subseteq A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\to \exists x\left(A\subseteq x\wedge x\circ x\subseteq x\right)$$
33		intexab	$$⊢\exists x\left(A\subseteq x\wedge x\circ x\subseteq x\right)\leftrightarrow \bigcap \left\{x|\left(A\subseteq x\wedge x\circ x\subseteq x\right)\right\}\in \mathrm{V}$$
34	32 33	sylib	$$⊢\left(A\subseteq A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\wedge \left(A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\circ \left(A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\subseteq A\cup \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)\to \bigcap \left\{x|\left(A\subseteq x\wedge x\circ x\subseteq x\right)\right\}\in \mathrm{V}$$
35	2 25 34	mp2an	$$⊢\bigcap \left\{x|\left(A\subseteq x\wedge x\circ x\subseteq x\right)\right\}\in \mathrm{V}$$