Theorem rclexi

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

	Ref	Expression
Hypothesis	rclexi.1	$$⊢A\in V$$
Assertion	rclexi	$$⊢\bigcap \left\{x|\left(A\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		rclexi.1	$$⊢A\in V$$
2		ssun1	$$⊢A\subseteq A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)$$
3		dmun	$$⊢\mathrm{dom}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)=\mathrm{dom}A\cup \mathrm{dom}\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)$$
4		dmresi	$$⊢\mathrm{dom}\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)=\mathrm{dom}A\cup \mathrm{ran}A$$
5	4	uneq2i	$$⊢\mathrm{dom}A\cup \mathrm{dom}\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)=\mathrm{dom}A\cup \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
6		ssun1	$$⊢\mathrm{dom}A\subseteq \mathrm{dom}A\cup \mathrm{ran}A$$
7		ssequn1	$$⊢\mathrm{dom}A\subseteq \mathrm{dom}A\cup \mathrm{ran}A\leftrightarrow \mathrm{dom}A\cup \left(\mathrm{dom}A\cup \mathrm{ran}A\right)=\mathrm{dom}A\cup \mathrm{ran}A$$
8	6 7	mpbi	$$⊢\mathrm{dom}A\cup \left(\mathrm{dom}A\cup \mathrm{ran}A\right)=\mathrm{dom}A\cup \mathrm{ran}A$$
9	3 5 8	3eqtri	$$⊢\mathrm{dom}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)=\mathrm{dom}A\cup \mathrm{ran}A$$
10		rnun	$$⊢\mathrm{ran}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)=\mathrm{ran}A\cup \mathrm{ran}\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)$$
11		rnresi	$$⊢\mathrm{ran}\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)=\mathrm{dom}A\cup \mathrm{ran}A$$
12	11	uneq2i	$$⊢\mathrm{ran}A\cup \mathrm{ran}\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)=\mathrm{ran}A\cup \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
13		ssun2	$$⊢\mathrm{ran}A\subseteq \mathrm{dom}A\cup \mathrm{ran}A$$
14		ssequn1	$$⊢\mathrm{ran}A\subseteq \mathrm{dom}A\cup \mathrm{ran}A\leftrightarrow \mathrm{ran}A\cup \left(\mathrm{dom}A\cup \mathrm{ran}A\right)=\mathrm{dom}A\cup \mathrm{ran}A$$
15	13 14	mpbi	$$⊢\mathrm{ran}A\cup \left(\mathrm{dom}A\cup \mathrm{ran}A\right)=\mathrm{dom}A\cup \mathrm{ran}A$$
16	10 12 15	3eqtri	$$⊢\mathrm{ran}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)=\mathrm{dom}A\cup \mathrm{ran}A$$
17	9 16	uneq12i	$$⊢\mathrm{dom}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)\cup \mathrm{ran}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)=\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\cup \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
18		unidm	$$⊢\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\cup \left(\mathrm{dom}A\cup \mathrm{ran}A\right)=\mathrm{dom}A\cup \mathrm{ran}A$$
19	17 18	eqtri	$$⊢\mathrm{dom}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)\cup \mathrm{ran}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)=\mathrm{dom}A\cup \mathrm{ran}A$$
20	19	reseq2i	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)\cup \mathrm{ran}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)\right)}={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}$$
21		ssun2	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\subseteq A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)$$
22	20 21	eqsstri	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)\cup \mathrm{ran}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)\right)}\subseteq A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)$$
23	1	elexi	$$⊢A\in \mathrm{V}$$
24		dmexg	$$⊢A\in V\to \mathrm{dom}A\in \mathrm{V}$$
25		rnexg	$$⊢A\in V\to \mathrm{ran}A\in \mathrm{V}$$
26		unexg	$$⊢\left(\mathrm{dom}A\in \mathrm{V}\wedge \mathrm{ran}A\in \mathrm{V}\right)\to \mathrm{dom}A\cup \mathrm{ran}A\in \mathrm{V}$$
27	24 25 26	syl2anc	$$⊢A\in V\to \mathrm{dom}A\cup \mathrm{ran}A\in \mathrm{V}$$
28	27	resiexd	$$⊢A\in V\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\in \mathrm{V}$$
29	1 28	ax-mp	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\in \mathrm{V}$$
30	23 29	unex	$$⊢A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\in \mathrm{V}$$
31		dmeq	$$⊢x=A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\to \mathrm{dom}x=\mathrm{dom}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)$$
32		rneq	$$⊢x=A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\to \mathrm{ran}x=\mathrm{ran}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)$$
33	31 32	uneq12d	$$⊢x=A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\to \mathrm{dom}x\cup \mathrm{ran}x=\mathrm{dom}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)\cup \mathrm{ran}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)$$
34	33	reseq2d	$$⊢x=A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)\cup \mathrm{ran}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)\right)}$$
35		id	$$⊢x=A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\to x=A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)$$
36	34 35	sseq12d	$$⊢x=A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\to \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\leftrightarrow {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)\cup \mathrm{ran}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)\right)}\subseteq A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)$$
37	36	cleq2lem	$$⊢x=A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\to \left(\left(A\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\leftrightarrow \left(A\subseteq A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)\cup \mathrm{ran}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)\right)}\subseteq A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)\right)$$
38	30 37	spcev	$$⊢\left(A\subseteq A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)\cup \mathrm{ran}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)\right)}\subseteq A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)\to \exists x\left(A\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)$$
39		intexab	$$⊢\exists x\left(A\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\leftrightarrow \bigcap \left\{x|\left(A\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\right\}\in \mathrm{V}$$
40	38 39	sylib	$$⊢\left(A\subseteq A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)\cup \mathrm{ran}\left(A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)\right)}\subseteq A\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\right)\right)\to \bigcap \left\{x|\left(A\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\right\}\in \mathrm{V}$$
41	2 22 40	mp2an	$$⊢\bigcap \left\{x|\left(A\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\right\}\in \mathrm{V}$$