Theorem tuslem

Description: Lemma for tusbas , tusunif , and tustopn . (Contributed by Thierry Arnoux, 5-Dec-2017) (Proof shortened by AV, 28-Oct-2024)

	Ref	Expression
Hypothesis	tuslem.k	$$⊢K=\mathrm{toUnifSp}\left(U\right)$$
Assertion	tuslem	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \left(X={\mathrm{Base}}_K\wedge U=\mathrm{UnifSet}\left(K\right)\wedge \mathrm{unifTop}\left(U\right)=\mathrm{TopOpen}\left(K\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		tuslem.k	$$⊢K=\mathrm{toUnifSp}\left(U\right)$$
2		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
3		tsetndxnbasendx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
4	3	necomi	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
5	2 4	setsnid	$$⊢{\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup U⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),U⟩\right\}}={\mathrm{Base}}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup U⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),U⟩\right\}\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{unifTop}\left(U\right)⟩\right)}$$
6		ustbas2	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to X=\mathrm{dom}\bigcup U$$
7		uniexg	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \bigcup U\in \mathrm{V}$$
8		dmexg	$$⊢\bigcup U\in \mathrm{V}\to \mathrm{dom}\bigcup U\in \mathrm{V}$$
9		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup U⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),U⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup U⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),U⟩\right\}$$
10		basendxltunifndx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}<\mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
11		unifndxnn	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)\in \mathbb{N}$$
12	9 10 11	2strbas1	$$⊢\mathrm{dom}\bigcup U\in \mathrm{V}\to \mathrm{dom}\bigcup U={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup U⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),U⟩\right\}}$$
13	7 8 12	3syl	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \mathrm{dom}\bigcup U={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup U⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),U⟩\right\}}$$
14	6 13	eqtrd	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to X={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup U⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),U⟩\right\}}$$
15		tusval	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \mathrm{toUnifSp}\left(U\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup U⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),U⟩\right\}\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{unifTop}\left(U\right)⟩$$
16	1 15	eqtrid	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to K=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup U⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),U⟩\right\}\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{unifTop}\left(U\right)⟩$$
17	16	fveq2d	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to {\mathrm{Base}}_K={\mathrm{Base}}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup U⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),U⟩\right\}\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{unifTop}\left(U\right)⟩\right)}$$
18	5 14 17	3eqtr4a	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to X={\mathrm{Base}}_K$$
19		unifid	$$⊢\mathrm{UnifSet}=\mathrm{Slot}\mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
20		unifndxntsetndx	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
21	19 20	setsnid	$$⊢\mathrm{UnifSet}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup U⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),U⟩\right\}\right)=\mathrm{UnifSet}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup U⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),U⟩\right\}\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{unifTop}\left(U\right)⟩\right)$$
22	9 10 11 19	2strop1	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to U=\mathrm{UnifSet}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup U⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),U⟩\right\}\right)$$
23	16	fveq2d	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \mathrm{UnifSet}\left(K\right)=\mathrm{UnifSet}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup U⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),U⟩\right\}\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{unifTop}\left(U\right)⟩\right)$$
24	21 22 23	3eqtr4a	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to U=\mathrm{UnifSet}\left(K\right)$$
25		prex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup U⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),U⟩\right\}\in \mathrm{V}$$
26		fvex	$$⊢\mathrm{unifTop}\left(U\right)\in \mathrm{V}$$
27		tsetid	$$⊢\mathrm{TopSet}=\mathrm{Slot}\mathrm{TopSet}\left(\mathrm{ndx}\right)$$
28	27	setsid	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup U⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),U⟩\right\}\in \mathrm{V}\wedge \mathrm{unifTop}\left(U\right)\in \mathrm{V}\right)\to \mathrm{unifTop}\left(U\right)=\mathrm{TopSet}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup U⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),U⟩\right\}\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{unifTop}\left(U\right)⟩\right)$$
29	25 26 28	mp2an	$$⊢\mathrm{unifTop}\left(U\right)=\mathrm{TopSet}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup U⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),U⟩\right\}\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{unifTop}\left(U\right)⟩\right)$$
30	16	fveq2d	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \mathrm{TopSet}\left(K\right)=\mathrm{TopSet}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup U⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),U⟩\right\}\mathrm{sSet}⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{unifTop}\left(U\right)⟩\right)$$
31	29 30	eqtr4id	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \mathrm{unifTop}\left(U\right)=\mathrm{TopSet}\left(K\right)$$
32		utopbas	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to X=\bigcup \mathrm{unifTop}\left(U\right)$$
33	31	unieqd	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \bigcup \mathrm{unifTop}\left(U\right)=\bigcup \mathrm{TopSet}\left(K\right)$$
34	32 18 33	3eqtr3rd	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \bigcup \mathrm{TopSet}\left(K\right)={\mathrm{Base}}_K$$
35	34	oveq2d	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \mathrm{TopSet}\left(K\right){\upharpoonright }_{𝑡}\bigcup \mathrm{TopSet}\left(K\right)=\mathrm{TopSet}\left(K\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_K$$
36		fvex	$$⊢\mathrm{TopSet}\left(K\right)\in \mathrm{V}$$
37		eqid	$$⊢\bigcup \mathrm{TopSet}\left(K\right)=\bigcup \mathrm{TopSet}\left(K\right)$$
38	37	restid	$$⊢\mathrm{TopSet}\left(K\right)\in \mathrm{V}\to \mathrm{TopSet}\left(K\right){\upharpoonright }_{𝑡}\bigcup \mathrm{TopSet}\left(K\right)=\mathrm{TopSet}\left(K\right)$$
39	36 38	ax-mp	$$⊢\mathrm{TopSet}\left(K\right){\upharpoonright }_{𝑡}\bigcup \mathrm{TopSet}\left(K\right)=\mathrm{TopSet}\left(K\right)$$
40		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
41		eqid	$$⊢\mathrm{TopSet}\left(K\right)=\mathrm{TopSet}\left(K\right)$$
42	40 41	topnval	$$⊢\mathrm{TopSet}\left(K\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_K=\mathrm{TopOpen}\left(K\right)$$
43	35 39 42	3eqtr3g	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \mathrm{TopSet}\left(K\right)=\mathrm{TopOpen}\left(K\right)$$
44	31 43	eqtrd	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \mathrm{unifTop}\left(U\right)=\mathrm{TopOpen}\left(K\right)$$
45	18 24 44	3jca	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \left(X={\mathrm{Base}}_K\wedge U=\mathrm{UnifSet}\left(K\right)\wedge \mathrm{unifTop}\left(U\right)=\mathrm{TopOpen}\left(K\right)\right)$$