Theorem clcnvlem

Description: When A , an upper bound of the closure, exists and certain substitutions hold the converse of the closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020)

	Ref	Expression
Hypotheses	clcnvlem.sub1	$$⊢\left(\phi \wedge x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\to \left(\chi \to \psi \right)$$
	clcnvlem.sub2	$$⊢\left(\phi \wedge y=x^{-1}\right)\to \left(\psi \to \chi \right)$$
	clcnvlem.sub3	$$⊢x=A\to \left(\psi \leftrightarrow \theta \right)$$
	clcnvlem.ssub	$$⊢\phi \to X\subseteq A$$
	clcnvlem.ubex	$$⊢\phi \to A\in \mathrm{V}$$
	clcnvlem.clex	$$⊢\phi \to \theta$$
Assertion	clcnvlem	$$⊢\phi \to {\bigcap \left\{x|\left(X\subseteq x\wedge \psi \right)\right\}}^{-1}=\bigcap \left\{y|\left(X^{-1}\subseteq y\wedge \chi \right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		clcnvlem.sub1	$$⊢\left(\phi \wedge x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\to \left(\chi \to \psi \right)$$
2		clcnvlem.sub2	$$⊢\left(\phi \wedge y=x^{-1}\right)\to \left(\psi \to \chi \right)$$
3		clcnvlem.sub3	$$⊢x=A\to \left(\psi \leftrightarrow \theta \right)$$
4		clcnvlem.ssub	$$⊢\phi \to X\subseteq A$$
5		clcnvlem.ubex	$$⊢\phi \to A\in \mathrm{V}$$
6		clcnvlem.clex	$$⊢\phi \to \theta$$
7	4 6	jca	$$⊢\phi \to \left(X\subseteq A\wedge \theta \right)$$
8	3	cleq2lem	$$⊢x=A\to \left(\left(X\subseteq x\wedge \psi \right)\leftrightarrow \left(X\subseteq A\wedge \theta \right)\right)$$
9	5 7 8	spcedv	$$⊢\phi \to \exists x\left(X\subseteq x\wedge \psi \right)$$
10	9	cnvintabd	$$⊢\phi \to {\bigcap \left\{x|\left(X\subseteq x\wedge \psi \right)\right\}}^{-1}=\bigcap \left\{z\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)|\exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right\}$$
11		df-rab	$$⊢\left\{z\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)|\exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right\}=\left\{z|\left(z\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)\wedge \exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right)\right\}$$
12		exsimpl	$$⊢\exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\to \exists xz=x^{-1}$$
13		relcnv	$$⊢\mathrm{Rel}{x}^{-1}$$
14		releq	$$⊢z=x^{-1}\to \left(\mathrm{Rel}z\leftrightarrow \mathrm{Rel}{x}^{-1}\right)$$
15	13 14	mpbiri	$$⊢z=x^{-1}\to \mathrm{Rel}z$$
16	15	exlimiv	$$⊢\exists xz=x^{-1}\to \mathrm{Rel}z$$
17	12 16	syl	$$⊢\exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\to \mathrm{Rel}z$$
18		df-rel	$$⊢\mathrm{Rel}z\leftrightarrow z\subseteq \mathrm{V}\times \mathrm{V}$$
19	17 18	sylib	$$⊢\exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\to z\subseteq \mathrm{V}\times \mathrm{V}$$
20		velpw	$$⊢z\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow z\subseteq \mathrm{V}\times \mathrm{V}$$
21	20	bicomi	$$⊢z\subseteq \mathrm{V}\times \mathrm{V}\leftrightarrow z\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)$$
22	19 21	sylib	$$⊢\exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\to z\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)$$
23	22	pm4.71ri	$$⊢\exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\leftrightarrow \left(z\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)\wedge \exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right)$$
24	23	bicomi	$$⊢\left(z\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)\wedge \exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right)\leftrightarrow \exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)$$
25	24	abbii	$$⊢\left\{z|\left(z\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)\wedge \exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right)\right\}=\left\{z|\exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right\}$$
26	11 25	eqtri	$$⊢\left\{z\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)|\exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right\}=\left\{z|\exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right\}$$
27	26	inteqi	$$⊢\bigcap \left\{z\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)|\exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right\}=\bigcap \left\{z|\exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right\}$$
28	27	a1i	$$⊢\phi \to \bigcap \left\{z\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)|\exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right\}=\bigcap \left\{z|\exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right\}$$
29		vex	$$⊢y\in \mathrm{V}$$
30	29	cnvex	$$⊢y^{-1}\in \mathrm{V}$$
31	30	cnvex	$$⊢{y^{-1}}^{-1}\in \mathrm{V}$$
32	31	a1i	$$⊢\phi \to {y^{-1}}^{-1}\in \mathrm{V}$$
33	5 4	ssexd	$$⊢\phi \to X\in \mathrm{V}$$
34	33	difexd	$$⊢\phi \to X\setminus {X^{-1}}^{-1}\in \mathrm{V}$$
35		unexg	$$⊢\left(y^{-1}\in \mathrm{V}\wedge X\setminus {X^{-1}}^{-1}\in \mathrm{V}\right)\to y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\in \mathrm{V}$$
36	30 34 35	sylancr	$$⊢\phi \to y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\in \mathrm{V}$$
37		inundif	$$⊢\left(X\cap {X^{-1}}^{-1}\right)\cup \left(X\setminus {X^{-1}}^{-1}\right)=X$$
38		cnvun	$$⊢{\left(\left(X\cap {X^{-1}}^{-1}\right)\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)}^{-1}={\left(X\cap {X^{-1}}^{-1}\right)}^{-1}\cup {\left(X\setminus {X^{-1}}^{-1}\right)}^{-1}$$
39	38	sseq1i	$$⊢{\left(\left(X\cap {X^{-1}}^{-1}\right)\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)}^{-1}\subseteq y\leftrightarrow {\left(X\cap {X^{-1}}^{-1}\right)}^{-1}\cup {\left(X\setminus {X^{-1}}^{-1}\right)}^{-1}\subseteq y$$
40	39	biimpi	$$⊢{\left(\left(X\cap {X^{-1}}^{-1}\right)\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)}^{-1}\subseteq y\to {\left(X\cap {X^{-1}}^{-1}\right)}^{-1}\cup {\left(X\setminus {X^{-1}}^{-1}\right)}^{-1}\subseteq y$$
41	40	unssad	$$⊢{\left(\left(X\cap {X^{-1}}^{-1}\right)\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)}^{-1}\subseteq y\to {\left(X\cap {X^{-1}}^{-1}\right)}^{-1}\subseteq y$$
42		relcnv	$$⊢\mathrm{Rel}{X^{-1}}^{-1}$$
43		relin2	$$⊢\mathrm{Rel}{X^{-1}}^{-1}\to \mathrm{Rel}\left(X\cap {X^{-1}}^{-1}\right)$$
44	42 43	ax-mp	$$⊢\mathrm{Rel}\left(X\cap {X^{-1}}^{-1}\right)$$
45		dfrel2	$$⊢\mathrm{Rel}\left(X\cap {X^{-1}}^{-1}\right)\leftrightarrow {{\left(X\cap {X^{-1}}^{-1}\right)}^{-1}}^{-1}=X\cap {X^{-1}}^{-1}$$
46	44 45	mpbi	$$⊢{{\left(X\cap {X^{-1}}^{-1}\right)}^{-1}}^{-1}=X\cap {X^{-1}}^{-1}$$
47		cnvss	$$⊢{\left(X\cap {X^{-1}}^{-1}\right)}^{-1}\subseteq y\to {{\left(X\cap {X^{-1}}^{-1}\right)}^{-1}}^{-1}\subseteq y^{-1}$$
48	46 47	eqsstrrid	$$⊢{\left(X\cap {X^{-1}}^{-1}\right)}^{-1}\subseteq y\to X\cap {X^{-1}}^{-1}\subseteq y^{-1}$$
49	41 48	syl	$$⊢{\left(\left(X\cap {X^{-1}}^{-1}\right)\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)}^{-1}\subseteq y\to X\cap {X^{-1}}^{-1}\subseteq y^{-1}$$
50		ssid	$$⊢X\setminus {X^{-1}}^{-1}\subseteq X\setminus {X^{-1}}^{-1}$$
51		unss12	$$⊢\left(X\cap {X^{-1}}^{-1}\subseteq y^{-1}\wedge X\setminus {X^{-1}}^{-1}\subseteq X\setminus {X^{-1}}^{-1}\right)\to \left(X\cap {X^{-1}}^{-1}\right)\cup \left(X\setminus {X^{-1}}^{-1}\right)\subseteq y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)$$
52	49 50 51	sylancl	$$⊢{\left(\left(X\cap {X^{-1}}^{-1}\right)\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)}^{-1}\subseteq y\to \left(X\cap {X^{-1}}^{-1}\right)\cup \left(X\setminus {X^{-1}}^{-1}\right)\subseteq y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)$$
53	52	a1i	$$⊢\left(X\cap {X^{-1}}^{-1}\right)\cup \left(X\setminus {X^{-1}}^{-1}\right)=X\to \left({\left(\left(X\cap {X^{-1}}^{-1}\right)\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)}^{-1}\subseteq y\to \left(X\cap {X^{-1}}^{-1}\right)\cup \left(X\setminus {X^{-1}}^{-1}\right)\subseteq y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)$$
54		cnveq	$$⊢\left(X\cap {X^{-1}}^{-1}\right)\cup \left(X\setminus {X^{-1}}^{-1}\right)=X\to {\left(\left(X\cap {X^{-1}}^{-1}\right)\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)}^{-1}=X^{-1}$$
55	54	sseq1d	$$⊢\left(X\cap {X^{-1}}^{-1}\right)\cup \left(X\setminus {X^{-1}}^{-1}\right)=X\to \left({\left(\left(X\cap {X^{-1}}^{-1}\right)\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)}^{-1}\subseteq y\leftrightarrow X^{-1}\subseteq y\right)$$
56		sseq1	$$⊢\left(X\cap {X^{-1}}^{-1}\right)\cup \left(X\setminus {X^{-1}}^{-1}\right)=X\to \left(\left(X\cap {X^{-1}}^{-1}\right)\cup \left(X\setminus {X^{-1}}^{-1}\right)\subseteq y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\leftrightarrow X\subseteq y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)$$
57	53 55 56	3imtr3d	$$⊢\left(X\cap {X^{-1}}^{-1}\right)\cup \left(X\setminus {X^{-1}}^{-1}\right)=X\to \left(X^{-1}\subseteq y\to X\subseteq y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)$$
58	37 57	ax-mp	$$⊢X^{-1}\subseteq y\to X\subseteq y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)$$
59		sseq2	$$⊢x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\to \left(X\subseteq x\leftrightarrow X\subseteq y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)$$
60	58 59	syl5ibr	$$⊢x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\to \left(X^{-1}\subseteq y\to X\subseteq x\right)$$
61	60	adantl	$$⊢\left(\phi \wedge x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\to \left(X^{-1}\subseteq y\to X\subseteq x\right)$$
62	61 1	anim12d	$$⊢\left(\phi \wedge x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\to \left(\left(X^{-1}\subseteq y\wedge \chi \right)\to \left(X\subseteq x\wedge \psi \right)\right)$$
63		cnvun	$$⊢{\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)}^{-1}={y^{-1}}^{-1}\cup {\left(X\setminus {X^{-1}}^{-1}\right)}^{-1}$$
64		cnvnonrel	$$⊢{\left(X\setminus {X^{-1}}^{-1}\right)}^{-1}=\varnothing$$
65		0ss	$$⊢\varnothing \subseteq {y^{-1}}^{-1}$$
66	64 65	eqsstri	$$⊢{\left(X\setminus {X^{-1}}^{-1}\right)}^{-1}\subseteq {y^{-1}}^{-1}$$
67		ssequn2	$$⊢{\left(X\setminus {X^{-1}}^{-1}\right)}^{-1}\subseteq {y^{-1}}^{-1}\leftrightarrow {y^{-1}}^{-1}\cup {\left(X\setminus {X^{-1}}^{-1}\right)}^{-1}={y^{-1}}^{-1}$$
68	66 67	mpbi	$$⊢{y^{-1}}^{-1}\cup {\left(X\setminus {X^{-1}}^{-1}\right)}^{-1}={y^{-1}}^{-1}$$
69	63 68	eqtr2i	$$⊢{y^{-1}}^{-1}={\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)}^{-1}$$
70		cnveq	$$⊢x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\to x^{-1}={\left(y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)}^{-1}$$
71	69 70	eqtr4id	$$⊢x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\to {y^{-1}}^{-1}=x^{-1}$$
72	71	adantl	$$⊢\left(\phi \wedge x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\to {y^{-1}}^{-1}=x^{-1}$$
73	62 72	jctild	$$⊢\left(\phi \wedge x=y^{-1}\cup \left(X\setminus {X^{-1}}^{-1}\right)\right)\to \left(\left(X^{-1}\subseteq y\wedge \chi \right)\to \left({y^{-1}}^{-1}=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right)$$
74	36 73	spcimedv	$$⊢\phi \to \left(\left(X^{-1}\subseteq y\wedge \chi \right)\to \exists x\left({y^{-1}}^{-1}=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right)$$
75	74	imp	$$⊢\left(\phi \wedge \left(X^{-1}\subseteq y\wedge \chi \right)\right)\to \exists x\left({y^{-1}}^{-1}=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)$$
76	75	adantlr	$$⊢\left(\left(\phi \wedge z={y^{-1}}^{-1}\right)\wedge \left(X^{-1}\subseteq y\wedge \chi \right)\right)\to \exists x\left({y^{-1}}^{-1}=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)$$
77		eqeq1	$$⊢z={y^{-1}}^{-1}\to \left(z=x^{-1}\leftrightarrow {y^{-1}}^{-1}=x^{-1}\right)$$
78	77	anbi1d	$$⊢z={y^{-1}}^{-1}\to \left(\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\leftrightarrow \left({y^{-1}}^{-1}=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right)$$
79	78	exbidv	$$⊢z={y^{-1}}^{-1}\to \left(\exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\leftrightarrow \exists x\left({y^{-1}}^{-1}=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right)$$
80	79	ad2antlr	$$⊢\left(\left(\phi \wedge z={y^{-1}}^{-1}\right)\wedge \left(X^{-1}\subseteq y\wedge \chi \right)\right)\to \left(\exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\leftrightarrow \exists x\left({y^{-1}}^{-1}=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right)$$
81	76 80	mpbird	$$⊢\left(\left(\phi \wedge z={y^{-1}}^{-1}\right)\wedge \left(X^{-1}\subseteq y\wedge \chi \right)\right)\to \exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)$$
82	81	ex	$$⊢\left(\phi \wedge z={y^{-1}}^{-1}\right)\to \left(\left(X^{-1}\subseteq y\wedge \chi \right)\to \exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right)$$
83		cnvcnvss	$$⊢{y^{-1}}^{-1}\subseteq y$$
84	83	a1i	$$⊢\phi \to {y^{-1}}^{-1}\subseteq y$$
85	32 82 84	intabssd	$$⊢\phi \to \bigcap \left\{z|\exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right\}\subseteq \bigcap \left\{y|\left(X^{-1}\subseteq y\wedge \chi \right)\right\}$$
86		vex	$$⊢z\in \mathrm{V}$$
87	86	a1i	$$⊢\phi \to z\in \mathrm{V}$$
88		eqtr	$$⊢\left(y=z\wedge z=x^{-1}\right)\to y=x^{-1}$$
89		cnvss	$$⊢X\subseteq x\to X^{-1}\subseteq x^{-1}$$
90		sseq2	$$⊢y=x^{-1}\to \left(X^{-1}\subseteq y\leftrightarrow X^{-1}\subseteq x^{-1}\right)$$
91	89 90	syl5ibr	$$⊢y=x^{-1}\to \left(X\subseteq x\to X^{-1}\subseteq y\right)$$
92	91	adantl	$$⊢\left(\phi \wedge y=x^{-1}\right)\to \left(X\subseteq x\to X^{-1}\subseteq y\right)$$
93	92 2	anim12d	$$⊢\left(\phi \wedge y=x^{-1}\right)\to \left(\left(X\subseteq x\wedge \psi \right)\to \left(X^{-1}\subseteq y\wedge \chi \right)\right)$$
94	93	ex	$$⊢\phi \to \left(y=x^{-1}\to \left(\left(X\subseteq x\wedge \psi \right)\to \left(X^{-1}\subseteq y\wedge \chi \right)\right)\right)$$
95	88 94	syl5	$$⊢\phi \to \left(\left(y=z\wedge z=x^{-1}\right)\to \left(\left(X\subseteq x\wedge \psi \right)\to \left(X^{-1}\subseteq y\wedge \chi \right)\right)\right)$$
96	95	impl	$$⊢\left(\left(\phi \wedge y=z\right)\wedge z=x^{-1}\right)\to \left(\left(X\subseteq x\wedge \psi \right)\to \left(X^{-1}\subseteq y\wedge \chi \right)\right)$$
97	96	expimpd	$$⊢\left(\phi \wedge y=z\right)\to \left(\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\to \left(X^{-1}\subseteq y\wedge \chi \right)\right)$$
98	97	exlimdv	$$⊢\left(\phi \wedge y=z\right)\to \left(\exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\to \left(X^{-1}\subseteq y\wedge \chi \right)\right)$$
99		ssid	$$⊢z\subseteq z$$
100	99	a1i	$$⊢\phi \to z\subseteq z$$
101	87 98 100	intabssd	$$⊢\phi \to \bigcap \left\{y|\left(X^{-1}\subseteq y\wedge \chi \right)\right\}\subseteq \bigcap \left\{z|\exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right\}$$
102	85 101	eqssd	$$⊢\phi \to \bigcap \left\{z|\exists x\left(z=x^{-1}\wedge \left(X\subseteq x\wedge \psi \right)\right)\right\}=\bigcap \left\{y|\left(X^{-1}\subseteq y\wedge \chi \right)\right\}$$
103	10 28 102	3eqtrd	$$⊢\phi \to {\bigcap \left\{x|\left(X\subseteq x\wedge \psi \right)\right\}}^{-1}=\bigcap \left\{y|\left(X^{-1}\subseteq y\wedge \chi \right)\right\}$$