Theorem rtrclexi

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

	Ref	Expression
Hypothesis	rtrclexi.1	$$⊢A\in V$$
Assertion	rtrclexi	$$⊢\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		rtrclexi.1	$$⊢A\in V$$
2		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)$$
3		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)$$
4		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)$$
5		cossxp	$$⊢A\circ A\subseteq \mathrm{dom}A\times \mathrm{ran}A$$
6		ssun1	$$⊢\mathrm{dom}A\subseteq \mathrm{dom}A\cup \mathrm{ran}A$$
7		ssun2	$$⊢\mathrm{ran}A\subseteq \mathrm{dom}A\cup \mathrm{ran}A$$
8		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)$$
9	6 7 8	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)$$
10	5 9	sstri	$$⊢A\circ A\subseteq \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
11		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$$
12		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$$
13		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)$$
14	12 7 13	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)$$
15	11 14	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)$$
16	10 15	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)$$
17	4 16	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)$$
18		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)$$
19		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)$$
20		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$$
21		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)$$
22	6 20 21	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)$$
23	19 22	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)$$
24		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)$$
25	23 24	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)$$
26	18 25	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)$$
27	17 26	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)$$
28	3 27	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)$$
29		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)$$
30	28 29	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)$$
31		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)$$
32	6 12	unssi	$$⊢\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)\subseteq \mathrm{dom}A\cup \mathrm{ran}A$$
33	31 32	eqsstri	$$⊢\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)\subseteq \mathrm{dom}A\cup \mathrm{ran}A$$
34		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)$$
35	7 20	unssi	$$⊢\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)\subseteq \mathrm{dom}A\cup \mathrm{ran}A$$
36	34 35	eqsstri	$$⊢\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)\subseteq \mathrm{dom}A\cup \mathrm{ran}A$$
37	33 36	unssi	$$⊢\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)\subseteq \mathrm{dom}A\cup \mathrm{ran}A$$
38		ssres2	$$⊢\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)\subseteq \mathrm{dom}A\cup \mathrm{ran}A\to {\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 {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}$$
39	37 38	ax-mp	$$⊢{\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 {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}$$
40		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)$$
41	39 40	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 \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)$$
42	41 29	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)$$
43		id	$$⊢\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)\to \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)$$
44	30 42 43	mp2an	$$⊢\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)$$
45	1	elexi	$$⊢A\in \mathrm{V}$$
46	45	dmex	$$⊢\mathrm{dom}A\in \mathrm{V}$$
47	45	rnex	$$⊢\mathrm{ran}A\in \mathrm{V}$$
48	46 47	unex	$$⊢\mathrm{dom}A\cup \mathrm{ran}A\in \mathrm{V}$$
49	48 48	xpex	$$⊢\left(\mathrm{dom}A\cup \mathrm{ran}A\right)\times \left(\mathrm{dom}A\cup \mathrm{ran}A\right)\in \mathrm{V}$$
50	45 49	unex	$$⊢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	50 60	spcev	$$⊢\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)$$
62		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}$$
63	61 62	sylib	$$⊢\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 \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}$$
64	2 44 63	mp2an	$$⊢\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}$$