Theorem rtrclex

Description: The reflexive-transitive closure of a set exists. (Contributed by RP, 1-Nov-2020)

	Ref	Expression
Assertion	rtrclex	$$⊢A\in \mathrm{V}\leftrightarrow \bigcap \left\{x|\left(A\subseteq x\wedge \left(x\circ x\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\right)\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ssun1	$$⊢A\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)$$
2		coundir	$$⊢\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\circ \left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)=\left(A\circ \left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\right)\cup \left(\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\circ \left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\right)$$
3		coundi	$$⊢A\circ \left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)=\left(A\circ A\right)\cup \left(A\circ \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)$$
4		cossxp	$$⊢A\circ A\subseteq \mathrm{dom}A\times \mathrm{ran}A$$
5		ssun1	$$⊢\mathrm{dom}A\subseteq \mathrm{dom}A\cup \mathrm{ran}A$$
6		ssun2	$$⊢\mathrm{ran}A\subseteq \mathrm{dom}A\cup \mathrm{ran}A$$
7		xpss12	$$⊢\left(\mathrm{dom}A\subseteq \mathrm{dom}A\cup \mathrm{ran}A\wedge \mathrm{ran}A\subseteq \mathrm{dom}A\cup \mathrm{ran}A\right)\to \mathrm{dom}A\times \mathrm{ran}A\subseteq \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
8	5 6 7	mp2an	$$⊢\mathrm{dom}A\times \mathrm{ran}A\subseteq \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
9	4 8	sstri	$$⊢A\circ A\subseteq \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
10		cossxp	$$⊢A\circ \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\subseteq \mathrm{dom}\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\times \mathrm{ran}A$$
11		dmxpss	$$⊢\mathrm{dom}\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\subseteq \mathrm{dom}A\cup \mathrm{ran}A$$
12		xpss12	$$⊢\left(\mathrm{dom}\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\subseteq \mathrm{dom}A\cup \mathrm{ran}A\wedge \mathrm{ran}A\subseteq \mathrm{dom}A\cup \mathrm{ran}A\right)\to \mathrm{dom}\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\times \mathrm{ran}A\subseteq \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
13	11 6 12	mp2an	$$⊢\mathrm{dom}\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\times \mathrm{ran}A\subseteq \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
14	10 13	sstri	$$⊢A\circ \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\subseteq \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
15	9 14	unssi	$$⊢\left(A\circ A\right)\cup \left(A\circ \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\subseteq \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
16	3 15	eqsstri	$$⊢A\circ \left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\subseteq \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
17		coundi	$$⊢\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\circ \left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)=\left(\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\circ A\right)\cup \left(\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\circ \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)$$
18		cossxp	$$⊢\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\circ A\subseteq \mathrm{dom}A\times \mathrm{ran}\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)$$
19		rnxpss	$$⊢\mathrm{ran}\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\subseteq \mathrm{dom}A\cup \mathrm{ran}A$$
20		xpss12	$$⊢\left(\mathrm{dom}A\subseteq \mathrm{dom}A\cup \mathrm{ran}A\wedge \mathrm{ran}\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\subseteq \mathrm{dom}A\cup \mathrm{ran}A\right)\to \mathrm{dom}A\times \mathrm{ran}\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\subseteq \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
21	5 19 20	mp2an	$$⊢\mathrm{dom}A\times \mathrm{ran}\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\subseteq \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
22	18 21	sstri	$$⊢\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\circ A\subseteq \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
23		xpidtr	$$⊢\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\circ \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\subseteq \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
24	22 23	unssi	$$⊢\left(\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\circ A\right)\cup \left(\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\circ \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\subseteq \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
25	17 24	eqsstri	$$⊢\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\circ \left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\subseteq \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
26	16 25	unssi	$$⊢\left(A\circ \left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\right)\cup \left(\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\circ \left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\right)\subseteq \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
27	2 26	eqsstri	$$⊢\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\circ \left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\subseteq \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
28		ssun2	$$⊢\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)$$
29	27 28	sstri	$$⊢\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\circ \left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)$$
30		dmun	$$⊢\mathrm{dom}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)=\mathrm{dom}A\cup \mathrm{dom}\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)$$
31		dmxpid	$$⊢\mathrm{dom}\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)=\mathrm{dom}A\cup \mathrm{ran}A$$
32	31	uneq2i	$$⊢\mathrm{dom}A\cup \mathrm{dom}\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)=\mathrm{dom}A\cup \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
33		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$$
34	5 33	mpbi	$$⊢\mathrm{dom}A\cup \left(\mathrm{dom}A\cup \mathrm{ran}A\right)=\mathrm{dom}A\cup \mathrm{ran}A$$
35	30 32 34	3eqtri	$$⊢\mathrm{dom}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)=\mathrm{dom}A\cup \mathrm{ran}A$$
36		rnun	$$⊢\mathrm{ran}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)=\mathrm{ran}A\cup \mathrm{ran}\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)$$
37		rnxpid	$$⊢\mathrm{ran}\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)=\mathrm{dom}A\cup \mathrm{ran}A$$
38	37	uneq2i	$$⊢\mathrm{ran}A\cup \mathrm{ran}\left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)=\mathrm{ran}A\cup \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
39		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$$
40	6 39	mpbi	$$⊢\mathrm{ran}A\cup \left(\mathrm{dom}A\cup \mathrm{ran}A\right)=\mathrm{dom}A\cup \mathrm{ran}A$$
41	36 38 40	3eqtri	$$⊢\mathrm{ran}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)=\mathrm{dom}A\cup \mathrm{ran}A$$
42	35 41	uneq12i	$$⊢\mathrm{dom}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\cup \mathrm{ran}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \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)$$
43		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$$
44	42 43	eqtri	$$⊢\mathrm{dom}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\cup \mathrm{ran}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)=\mathrm{dom}A\cup \mathrm{ran}A$$
45	44	reseq2i	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\cup \mathrm{ran}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\right)}={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}$$
46		idssxp	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\subseteq \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
47	45 46	eqsstri	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\cup \mathrm{ran}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\right)}\subseteq \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
48	47 28	sstri	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\cup \mathrm{ran}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\right)}\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)$$
49	29 48	pm3.2i	$$⊢\left(\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\circ \left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\cup \mathrm{ran}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\right)}\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)$$
50		rtrclexlem	$$⊢A\in \mathrm{V}\to A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\in \mathrm{V}$$
51		id	$$⊢x=A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\to x=A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)$$
52	51 51	coeq12d	$$⊢x=A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\to x\circ x=\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\circ \left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)$$
53	52 51	sseq12d	$$⊢x=A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\to \left(x\circ x\subseteq x\leftrightarrow \left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\circ \left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)$$
54		dmeq	$$⊢x=A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\to \mathrm{dom}x=\mathrm{dom}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)$$
55		rneq	$$⊢x=A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\to \mathrm{ran}x=\mathrm{ran}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)$$
56	54 55	uneq12d	$$⊢x=A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\to \mathrm{dom}x\cup \mathrm{ran}x=\mathrm{dom}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\cup \mathrm{ran}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)$$
57	56	reseq2d	$$⊢x=A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \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(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\cup \mathrm{ran}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\right)}$$
58	57 51	sseq12d	$$⊢x=A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \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(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\cup \mathrm{ran}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\right)}\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)$$
59	53 58	anbi12d	$$⊢x=A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\to \left(\left(x\circ x\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\leftrightarrow \left(\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\circ \left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\cup \mathrm{ran}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\right)}\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\right)$$
60	59	cleq2lem	$$⊢x=A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\to \left(\left(A\subseteq x\wedge \left(x\circ x\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\right)\leftrightarrow \left(A\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\wedge \left(\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\circ \left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\cup \mathrm{ran}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\right)}\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\right)\right)$$
61	60	biimprd	$$⊢x=A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\to \left(\left(A\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\wedge \left(\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\circ \left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\cup \mathrm{ran}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\right)}\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\right)\to \left(A\subseteq x\wedge \left(x\circ x\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\right)\right)$$
62	61	adantl	$$⊢\left(A\in \mathrm{V}\wedge x=A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\to \left(\left(A\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\wedge \left(\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\circ \left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\cup \mathrm{ran}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\right)}\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\right)\to \left(A\subseteq x\wedge \left(x\circ x\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\right)\right)$$
63	50 62	spcimedv	$$⊢A\in \mathrm{V}\to \left(\left(A\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\wedge \left(\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\circ \left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\cup \mathrm{ran}\left(A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\right)}\subseteq A\cup \left(\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\right)\right)\right)\to \exists x\left(A\subseteq x\wedge \left(x\circ x\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\right)\right)$$
64	1 49 63	mp2ani	$$⊢A\in \mathrm{V}\to \exists x\left(A\subseteq x\wedge \left(x\circ x\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\right)$$
65		exsimpl	$$⊢\exists x\left(A\subseteq x\wedge \left(x\circ x\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\right)\to \exists xA\subseteq x$$
66		vex	$$⊢x\in \mathrm{V}$$
67	66	ssex	$$⊢A\subseteq x\to A\in \mathrm{V}$$
68	67	exlimiv	$$⊢\exists xA\subseteq x\to A\in \mathrm{V}$$
69	65 68	syl	$$⊢\exists x\left(A\subseteq x\wedge \left(x\circ x\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\right)\to A\in \mathrm{V}$$
70	64 69	impbii	$$⊢A\in \mathrm{V}\leftrightarrow \exists x\left(A\subseteq x\wedge \left(x\circ x\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\right)$$
71		intexab	$$⊢\exists x\left(A\subseteq x\wedge \left(x\circ x\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\right)\leftrightarrow \bigcap \left\{x|\left(A\subseteq x\wedge \left(x\circ x\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\right)\right\}\in \mathrm{V}$$
72	70 71	bitri	$$⊢A\in \mathrm{V}\leftrightarrow \bigcap \left\{x|\left(A\subseteq x\wedge \left(x\circ x\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\right)\right\}\in \mathrm{V}$$