Theorem cnvrcl0

Description: The converse of the reflexive closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020)

	Ref	Expression
Assertion	cnvrcl0	$$⊢X\in V\to {\bigcap \left\{x|\left(X\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\right\}}^{-1}=\bigcap \left\{y|\left(X^{-1}\subseteq y\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}y\cup \mathrm{ran}y\right)}\subseteq y\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		cnvresid	$$⊢{\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}y\cup \mathrm{ran}y\right)}\right)}^{-1}={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}y\cup \mathrm{ran}y\right)}$$
2		cnvnonrel	$$⊢{\left(X\setminus {X^{-1}}^{-1}\right)}^{-1}=\varnothing$$
3		cnv0	$$⊢{\varnothing }^{-1}=\varnothing$$
4	2 3	eqtr4i	$$⊢{\left(X\setminus {X^{-1}}^{-1}\right)}^{-1}={\varnothing }^{-1}$$
5	4	dmeqi	$$⊢\mathrm{dom}{\left(X\setminus {X^{-1}}^{-1}\right)}^{-1}=\mathrm{dom}{\varnothing }^{-1}$$
6		df-rn	$$⊢\mathrm{ran}\left(X\setminus {X^{-1}}^{-1}\right)=\mathrm{dom}{\left(X\setminus {X^{-1}}^{-1}\right)}^{-1}$$
7		df-rn	$$⊢\mathrm{ran}\varnothing =\mathrm{dom}{\varnothing }^{-1}$$
8	5 6 7	3eqtr4i	$$⊢\mathrm{ran}\left(X\setminus {X^{-1}}^{-1}\right)=\mathrm{ran}\varnothing$$
9		0ss	$$⊢\varnothing \subseteq y^{-1}$$
10	9	rnssi	$$⊢\mathrm{ran}\varnothing \subseteq \mathrm{ran}{y}^{-1}$$
11	8 10	eqsstri	$$⊢\mathrm{ran}\left(X\setminus {X^{-1}}^{-1}\right)\subseteq \mathrm{ran}{y}^{-1}$$
12		ssequn2	$$⊢\mathrm{ran}\left(X\setminus {X^{-1}}^{-1}\right)\subseteq \mathrm{ran}{y}^{-1}\leftrightarrow \mathrm{ran}{y}^{-1}\cup \mathrm{ran}\left(X\setminus {X^{-1}}^{-1}\right)=\mathrm{ran}{y}^{-1}$$
13	11 12	mpbi	$$⊢\mathrm{ran}{y}^{-1}\cup \mathrm{ran}\left(X\setminus {X^{-1}}^{-1}\right)=\mathrm{ran}{y}^{-1}$$
14		rnun	$$⊢\mathrm{ran}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)=\mathrm{ran}{y}^{-1}\cup \mathrm{ran}\left(X\setminus {X^{-1}}^{-1}\right)$$
15		dfdm4	$$⊢\mathrm{dom}y=\mathrm{ran}{y}^{-1}$$
16	13 14 15	3eqtr4ri	$$⊢\mathrm{dom}y=\mathrm{ran}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)$$
17	4	rneqi	$$⊢\mathrm{ran}{\left(X\setminus {X^{-1}}^{-1}\right)}^{-1}=\mathrm{ran}{\varnothing }^{-1}$$
18		dfdm4	$$⊢\mathrm{dom}\left(X\setminus {X^{-1}}^{-1}\right)=\mathrm{ran}{\left(X\setminus {X^{-1}}^{-1}\right)}^{-1}$$
19		dfdm4	$$⊢\mathrm{dom}\varnothing =\mathrm{ran}{\varnothing }^{-1}$$
20	17 18 19	3eqtr4i	$$⊢\mathrm{dom}\left(X\setminus {X^{-1}}^{-1}\right)=\mathrm{dom}\varnothing$$
21		dmss	$$⊢\varnothing \subseteq y^{-1}\to \mathrm{dom}\varnothing \subseteq \mathrm{dom}{y}^{-1}$$
22	9 21	ax-mp	$$⊢\mathrm{dom}\varnothing \subseteq \mathrm{dom}{y}^{-1}$$
23	20 22	eqsstri	$$⊢\mathrm{dom}\left(X\setminus {X^{-1}}^{-1}\right)\subseteq \mathrm{dom}{y}^{-1}$$
24		ssequn2	$$⊢\mathrm{dom}\left(X\setminus {X^{-1}}^{-1}\right)\subseteq \mathrm{dom}{y}^{-1}\leftrightarrow \mathrm{dom}{y}^{-1}\cup \mathrm{dom}\left(X\setminus {X^{-1}}^{-1}\right)=\mathrm{dom}{y}^{-1}$$
25	23 24	mpbi	$$⊢\mathrm{dom}{y}^{-1}\cup \mathrm{dom}\left(X\setminus {X^{-1}}^{-1}\right)=\mathrm{dom}{y}^{-1}$$
26		dmun	$$⊢\mathrm{dom}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)=\mathrm{dom}{y}^{-1}\cup \mathrm{dom}\left(X\setminus {X^{-1}}^{-1}\right)$$
27		df-rn	$$⊢\mathrm{ran}y=\mathrm{dom}{y}^{-1}$$
28	25 26 27	3eqtr4ri	$$⊢\mathrm{ran}y=\mathrm{dom}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)$$
29	16 28	uneq12i	$$⊢\mathrm{dom}y\cup \mathrm{ran}y=\mathrm{ran}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\cup \mathrm{dom}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)$$
30	29	equncomi	$$⊢\mathrm{dom}y\cup \mathrm{ran}y=\mathrm{dom}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\cup \mathrm{ran}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)$$
31	30	reseq2i	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}y\cup \mathrm{ran}y\right)}={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\cup \mathrm{ran}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\right)}$$
32	1 31	eqtr2i	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\cup \mathrm{ran}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\right)}={\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}y\cup \mathrm{ran}y\right)}\right)}^{-1}$$
33		cnvss	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}y\cup \mathrm{ran}y\right)}\subseteq y\to {\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}y\cup \mathrm{ran}y\right)}\right)}^{-1}\subseteq y^{-1}$$
34	32 33	eqsstrid	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}y\cup \mathrm{ran}y\right)}\subseteq y\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\cup \mathrm{ran}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\right)}\subseteq y^{-1}$$
35		ssun1	$$⊢y^{-1}\subseteq y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)$$
36	34 35	sstrdi	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}y\cup \mathrm{ran}y\right)}\subseteq y\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\cup \mathrm{ran}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\right)}\subseteq y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)$$
37		dmeq	$$⊢x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\to \mathrm{dom}x=\mathrm{dom}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)$$
38		rneq	$$⊢x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\to \mathrm{ran}x=\mathrm{ran}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)$$
39	37 38	uneq12d	$$⊢x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\to \mathrm{dom}x\cup \mathrm{ran}x=\mathrm{dom}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\cup \mathrm{ran}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)$$
40	39	reseq2d	$$⊢x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\cup \mathrm{ran}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\right)}$$
41		id	$$⊢x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\to x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)$$
42	40 41	sseq12d	$$⊢x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\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(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\cup \mathrm{ran}\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\right)}\subseteq y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)$$
43	36 42	imbitrrid	$$⊢x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\to \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}y\cup \mathrm{ran}y\right)}\subseteq y\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)$$
44	43	adantl	$$⊢\left(X\in V\wedge x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\to \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}y\cup \mathrm{ran}y\right)}\subseteq y\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)$$
45		cnvresid	$$⊢{\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\right)}^{-1}={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}$$
46		dfdm4	$$⊢\mathrm{dom}x=\mathrm{ran}{x}^{-1}$$
47		df-rn	$$⊢\mathrm{ran}x=\mathrm{dom}{x}^{-1}$$
48	46 47	uneq12i	$$⊢\mathrm{dom}x\cup \mathrm{ran}x=\mathrm{ran}{x}^{-1}\cup \mathrm{dom}{x}^{-1}$$
49	48	equncomi	$$⊢\mathrm{dom}x\cup \mathrm{ran}x=\mathrm{dom}{x}^{-1}\cup \mathrm{ran}{x}^{-1}$$
50	49	reseq2i	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}{x}^{-1}\cup \mathrm{ran}{x}^{-1}\right)}$$
51	45 50	eqtr2i	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}{x}^{-1}\cup \mathrm{ran}{x}^{-1}\right)}={\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\right)}^{-1}$$
52		cnvss	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\to {\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\right)}^{-1}\subseteq x^{-1}$$
53	51 52	eqsstrid	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}{x}^{-1}\cup \mathrm{ran}{x}^{-1}\right)}\subseteq x^{-1}$$
54		dmeq	$$⊢y=x^{-1}\to \mathrm{dom}y=\mathrm{dom}{x}^{-1}$$
55		rneq	$$⊢y=x^{-1}\to \mathrm{ran}y=\mathrm{ran}{x}^{-1}$$
56	54 55	uneq12d	$$⊢y=x^{-1}\to \mathrm{dom}y\cup \mathrm{ran}y=\mathrm{dom}{x}^{-1}\cup \mathrm{ran}{x}^{-1}$$
57	56	reseq2d	$$⊢y=x^{-1}\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}y\cup \mathrm{ran}y\right)}={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}{x}^{-1}\cup \mathrm{ran}{x}^{-1}\right)}$$
58		id	$$⊢y=x^{-1}\to y=x^{-1}$$
59	57 58	sseq12d	$$⊢y=x^{-1}\to \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}y\cup \mathrm{ran}y\right)}\subseteq y\leftrightarrow {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}{x}^{-1}\cup \mathrm{ran}{x}^{-1}\right)}\subseteq x^{-1}\right)$$
60	53 59	imbitrrid	$$⊢y=x^{-1}\to \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}y\cup \mathrm{ran}y\right)}\subseteq y\right)$$
61	60	adantl	$$⊢\left(X\in V\wedge y=x^{-1}\right)\to \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}y\cup \mathrm{ran}y\right)}\subseteq y\right)$$
62		dmeq	$$⊢x=X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\to \mathrm{dom}x=\mathrm{dom}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)$$
63		rneq	$$⊢x=X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\to \mathrm{ran}x=\mathrm{ran}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)$$
64	62 63	uneq12d	$$⊢x=X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\to \mathrm{dom}x\cup \mathrm{ran}x=\mathrm{dom}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\cup \mathrm{ran}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)$$
65	64	reseq2d	$$⊢x=X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\cup \mathrm{ran}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\right)}$$
66		id	$$⊢x=X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\to x=X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)$$
67	65 66	sseq12d	$$⊢x=X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\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(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\cup \mathrm{ran}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\right)}\subseteq X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)$$
68		ssun1	$$⊢X\subseteq X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)$$
69	68	a1i	$$⊢X\in V\to X\subseteq X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)$$
70		dmexg	$$⊢X\in V\to \mathrm{dom}X\in \mathrm{V}$$
71		rnexg	$$⊢X\in V\to \mathrm{ran}X\in \mathrm{V}$$
72	70 71	unexd	$$⊢X\in V\to \mathrm{dom}X\cup \mathrm{ran}X\in \mathrm{V}$$
73	72	resiexd	$$⊢X\in V\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\in \mathrm{V}$$
74		unexg	$$⊢\left(X\in V\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\in \mathrm{V}\right)\to X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\in \mathrm{V}$$
75	73 74	mpdan	$$⊢X\in V\to X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\in \mathrm{V}$$
76		dmun	$$⊢\mathrm{dom}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)=\mathrm{dom}X\cup \mathrm{dom}\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)$$
77		ssun1	$$⊢\mathrm{dom}X\subseteq \mathrm{dom}X\cup \mathrm{ran}X$$
78		resdmss	$$⊢\mathrm{dom}\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\subseteq \mathrm{dom}X\cup \mathrm{ran}X$$
79	77 78	unssi	$$⊢\mathrm{dom}X\cup \mathrm{dom}\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\subseteq \mathrm{dom}X\cup \mathrm{ran}X$$
80	76 79	eqsstri	$$⊢\mathrm{dom}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\subseteq \mathrm{dom}X\cup \mathrm{ran}X$$
81		rnun	$$⊢\mathrm{ran}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)=\mathrm{ran}X\cup \mathrm{ran}\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)$$
82		ssun2	$$⊢\mathrm{ran}X\subseteq \mathrm{dom}X\cup \mathrm{ran}X$$
83		rnresi	$$⊢\mathrm{ran}\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)=\mathrm{dom}X\cup \mathrm{ran}X$$
84	83	eqimssi	$$⊢\mathrm{ran}\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\subseteq \mathrm{dom}X\cup \mathrm{ran}X$$
85	82 84	unssi	$$⊢\mathrm{ran}X\cup \mathrm{ran}\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\subseteq \mathrm{dom}X\cup \mathrm{ran}X$$
86	81 85	eqsstri	$$⊢\mathrm{ran}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\subseteq \mathrm{dom}X\cup \mathrm{ran}X$$
87	80 86	pm3.2i	$$⊢\left(\mathrm{dom}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\subseteq \mathrm{dom}X\cup \mathrm{ran}X\wedge \mathrm{ran}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\subseteq \mathrm{dom}X\cup \mathrm{ran}X\right)$$
88		unss	$$⊢\left(\mathrm{dom}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\subseteq \mathrm{dom}X\cup \mathrm{ran}X\wedge \mathrm{ran}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\subseteq \mathrm{dom}X\cup \mathrm{ran}X\right)\leftrightarrow \mathrm{dom}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\cup \mathrm{ran}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\subseteq \mathrm{dom}X\cup \mathrm{ran}X$$
89		ssres2	$$⊢\mathrm{dom}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\cup \mathrm{ran}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\subseteq \mathrm{dom}X\cup \mathrm{ran}X\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\cup \mathrm{ran}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\right)}\subseteq {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}$$
90	88 89	sylbi	$$⊢\left(\mathrm{dom}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\subseteq \mathrm{dom}X\cup \mathrm{ran}X\wedge \mathrm{ran}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\subseteq \mathrm{dom}X\cup \mathrm{ran}X\right)\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\cup \mathrm{ran}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\right)}\subseteq {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}$$
91		ssun4	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\cup \mathrm{ran}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\right)}\subseteq {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\cup \mathrm{ran}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\right)}\subseteq X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)$$
92	87 90 91	mp2b	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\cup \mathrm{ran}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\right)}\subseteq X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)$$
93	92	a1i	$$⊢X\in V\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\cup \mathrm{ran}\left(X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)\right)\right)}\subseteq X\cup \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}X\cup \mathrm{ran}X\right)}\right)$$
94	44 61 67 69 75 93	clcnvlem	$$⊢X\in V\to {\bigcap \left\{x|\left(X\subseteq x\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}x\cup \mathrm{ran}x\right)}\subseteq x\right)\right\}}^{-1}=\bigcap \left\{y|\left(X^{-1}\subseteq y\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}y\cup \mathrm{ran}y\right)}\subseteq y\right)\right\}$$