Theorem cnvtrcl0

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

	Ref	Expression
Assertion	cnvtrcl0	$$⊢X\in V\to {\bigcap \left\{x|\left(X\subseteq x\wedge x\circ x\subseteq x\right)\right\}}^{-1}=\bigcap \left\{y|\left(X^{-1}\subseteq y\wedge y\circ y\subseteq y\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		cnvco	$$⊢{\left(y\circ y\right)}^{-1}=y^{-1}\circ y^{-1}$$
2		cnvss	$$⊢y\circ y\subseteq y\to {\left(y\circ y\right)}^{-1}\subseteq y^{-1}$$
3	1 2	eqsstrrid	$$⊢y\circ y\subseteq y\to y^{-1}\circ y^{-1}\subseteq y^{-1}$$
4		coundir	$$⊢\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\circ \left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)=\left(y^{-1}\circ \left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\right)\cup \left(\left(X\setminus {X^{-1}}^{-1}\right)\circ \left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\right)$$
5		coundi	$$⊢y^{-1}\circ \left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)=\left(y^{-1}\circ y^{-1}\right)\cup \left(y^{-1}\circ \left(X\setminus {X^{-1}}^{-1}\right)\right)$$
6		ssid	$$⊢y^{-1}\circ y^{-1}\subseteq y^{-1}\circ y^{-1}$$
7		cononrel2	$$⊢y^{-1}\circ \left(X\setminus {X^{-1}}^{-1}\right)=\varnothing$$
8		0ss	$$⊢\varnothing \subseteq y^{-1}\circ y^{-1}$$
9	7 8	eqsstri	$$⊢y^{-1}\circ \left(X\setminus {X^{-1}}^{-1}\right)\subseteq y^{-1}\circ y^{-1}$$
10	6 9	unssi	$$⊢\left(y^{-1}\circ y^{-1}\right)\cup \left(y^{-1}\circ \left(X\setminus {X^{-1}}^{-1}\right)\right)\subseteq y^{-1}\circ y^{-1}$$
11	5 10	eqsstri	$$⊢y^{-1}\circ \left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\subseteq y^{-1}\circ y^{-1}$$
12		cononrel1	$$⊢\left(X\setminus {X^{-1}}^{-1}\right)\circ \left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)=\varnothing$$
13	12 8	eqsstri	$$⊢\left(X\setminus {X^{-1}}^{-1}\right)\circ \left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\subseteq y^{-1}\circ y^{-1}$$
14	11 13	unssi	$$⊢\left(y^{-1}\circ \left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\right)\cup \left(\left(X\setminus {X^{-1}}^{-1}\right)\circ \left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\right)\subseteq y^{-1}\circ y^{-1}$$
15	4 14	eqsstri	$$⊢\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\circ \left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\subseteq y^{-1}\circ y^{-1}$$
16		id	$$⊢y^{-1}\circ y^{-1}\subseteq y^{-1}\to y^{-1}\circ y^{-1}\subseteq y^{-1}$$
17	15 16	sstrid	$$⊢y^{-1}\circ y^{-1}\subseteq y^{-1}\to \left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\circ \left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\subseteq y^{-1}$$
18		ssun3	$$⊢\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\circ \left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\subseteq y^{-1}\to \left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\circ \left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\subseteq y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)$$
19	3 17 18	3syl	$$⊢y\circ y\subseteq y\to \left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\circ \left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\subseteq y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)$$
20		id	$$⊢x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\to x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)$$
21	20 20	coeq12d	$$⊢x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\to x\circ x=\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\circ \left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)$$
22	21 20	sseq12d	$$⊢x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\to \left(x\circ x\subseteq x\leftrightarrow \left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\circ \left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\subseteq y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)$$
23	19 22	imbitrrid	$$⊢x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\to \left(y\circ y\subseteq y\to x\circ x\subseteq x\right)$$
24	23	adantl	$$⊢\left(X\in V\wedge x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\to \left(y\circ y\subseteq y\to x\circ x\subseteq x\right)$$
25		cnvco	$$⊢{\left(x\circ x\right)}^{-1}=x^{-1}\circ x^{-1}$$
26		cnvss	$$⊢x\circ x\subseteq x\to {\left(x\circ x\right)}^{-1}\subseteq x^{-1}$$
27	25 26	eqsstrrid	$$⊢x\circ x\subseteq x\to x^{-1}\circ x^{-1}\subseteq x^{-1}$$
28		id	$$⊢y=x^{-1}\to y=x^{-1}$$
29	28 28	coeq12d	$$⊢y=x^{-1}\to y\circ y=x^{-1}\circ x^{-1}$$
30	29 28	sseq12d	$$⊢y=x^{-1}\to \left(y\circ y\subseteq y\leftrightarrow x^{-1}\circ x^{-1}\subseteq x^{-1}\right)$$
31	27 30	imbitrrid	$$⊢y=x^{-1}\to \left(x\circ x\subseteq x\to y\circ y\subseteq y\right)$$
32	31	adantl	$$⊢\left(X\in V\wedge y=x^{-1}\right)\to \left(x\circ x\subseteq x\to y\circ y\subseteq y\right)$$
33		id	$$⊢x=X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\to x=X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)$$
34	33 33	coeq12d	$$⊢x=X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\to x\circ x=\left(X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)\circ \left(X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)$$
35	34 33	sseq12d	$$⊢x=X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\to \left(x\circ x\subseteq x\leftrightarrow \left(X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)\circ \left(X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)\subseteq X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)$$
36		ssun1	$$⊢X\subseteq X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)$$
37	36	a1i	$$⊢X\in V\to X\subseteq X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)$$
38		trclexlem	$$⊢X\in V\to X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\in \mathrm{V}$$
39		coundir	$$⊢\left(X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)\circ \left(X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)=\left(X\circ \left(X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)\right)\cup \left(\left(\mathrm{dom}X\times \mathrm{ran}X\right)\circ \left(X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)\right)$$
40		coundi	$$⊢X\circ \left(X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)=\left(X\circ X\right)\cup \left(X\circ \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)$$
41		cossxp	$$⊢X\circ X\subseteq \mathrm{dom}X\times \mathrm{ran}X$$
42		cossxp	$$⊢X\circ \left(\mathrm{dom}X\times \mathrm{ran}X\right)\subseteq \mathrm{dom}\left(\mathrm{dom}X\times \mathrm{ran}X\right)\times \mathrm{ran}X$$
43		dmxpss	$$⊢\mathrm{dom}\left(\mathrm{dom}X\times \mathrm{ran}X\right)\subseteq \mathrm{dom}X$$
44		xpss1	$$⊢\mathrm{dom}\left(\mathrm{dom}X\times \mathrm{ran}X\right)\subseteq \mathrm{dom}X\to \mathrm{dom}\left(\mathrm{dom}X\times \mathrm{ran}X\right)\times \mathrm{ran}X\subseteq \mathrm{dom}X\times \mathrm{ran}X$$
45	43 44	ax-mp	$$⊢\mathrm{dom}\left(\mathrm{dom}X\times \mathrm{ran}X\right)\times \mathrm{ran}X\subseteq \mathrm{dom}X\times \mathrm{ran}X$$
46	42 45	sstri	$$⊢X\circ \left(\mathrm{dom}X\times \mathrm{ran}X\right)\subseteq \mathrm{dom}X\times \mathrm{ran}X$$
47	41 46	unssi	$$⊢\left(X\circ X\right)\cup \left(X\circ \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)\subseteq \mathrm{dom}X\times \mathrm{ran}X$$
48	40 47	eqsstri	$$⊢X\circ \left(X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)\subseteq \mathrm{dom}X\times \mathrm{ran}X$$
49		coundi	$$⊢\left(\mathrm{dom}X\times \mathrm{ran}X\right)\circ \left(X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)=\left(\left(\mathrm{dom}X\times \mathrm{ran}X\right)\circ X\right)\cup \left(\left(\mathrm{dom}X\times \mathrm{ran}X\right)\circ \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)$$
50		cossxp	$$⊢\left(\mathrm{dom}X\times \mathrm{ran}X\right)\circ X\subseteq \mathrm{dom}X\times \mathrm{ran}\left(\mathrm{dom}X\times \mathrm{ran}X\right)$$
51		rnxpss	$$⊢\mathrm{ran}\left(\mathrm{dom}X\times \mathrm{ran}X\right)\subseteq \mathrm{ran}X$$
52		xpss2	$$⊢\mathrm{ran}\left(\mathrm{dom}X\times \mathrm{ran}X\right)\subseteq \mathrm{ran}X\to \mathrm{dom}X\times \mathrm{ran}\left(\mathrm{dom}X\times \mathrm{ran}X\right)\subseteq \mathrm{dom}X\times \mathrm{ran}X$$
53	51 52	ax-mp	$$⊢\mathrm{dom}X\times \mathrm{ran}\left(\mathrm{dom}X\times \mathrm{ran}X\right)\subseteq \mathrm{dom}X\times \mathrm{ran}X$$
54	50 53	sstri	$$⊢\left(\mathrm{dom}X\times \mathrm{ran}X\right)\circ X\subseteq \mathrm{dom}X\times \mathrm{ran}X$$
55		xptrrel	$$⊢\left(\mathrm{dom}X\times \mathrm{ran}X\right)\circ \left(\mathrm{dom}X\times \mathrm{ran}X\right)\subseteq \mathrm{dom}X\times \mathrm{ran}X$$
56	54 55	unssi	$$⊢\left(\left(\mathrm{dom}X\times \mathrm{ran}X\right)\circ X\right)\cup \left(\left(\mathrm{dom}X\times \mathrm{ran}X\right)\circ \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)\subseteq \mathrm{dom}X\times \mathrm{ran}X$$
57	49 56	eqsstri	$$⊢\left(\mathrm{dom}X\times \mathrm{ran}X\right)\circ \left(X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)\subseteq \mathrm{dom}X\times \mathrm{ran}X$$
58	48 57	unssi	$$⊢\left(X\circ \left(X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)\right)\cup \left(\left(\mathrm{dom}X\times \mathrm{ran}X\right)\circ \left(X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)\right)\subseteq \mathrm{dom}X\times \mathrm{ran}X$$
59	39 58	eqsstri	$$⊢\left(X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)\circ \left(X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)\subseteq \mathrm{dom}X\times \mathrm{ran}X$$
60		ssun2	$$⊢\mathrm{dom}X\times \mathrm{ran}X\subseteq X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)$$
61	59 60	sstri	$$⊢\left(X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)\circ \left(X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)\subseteq X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)$$
62	61	a1i	$$⊢X\in V\to \left(X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)\circ \left(X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)\right)\subseteq X\cup \left(\mathrm{dom}X\times \mathrm{ran}X\right)$$
63	24 32 35 37 38 62	clcnvlem	$$⊢X\in V\to {\bigcap \left\{x|\left(X\subseteq x\wedge x\circ x\subseteq x\right)\right\}}^{-1}=\bigcap \left\{y|\left(X^{-1}\subseteq y\wedge y\circ y\subseteq y\right)\right\}$$