Theorem tuslemOLD

Description: Obsolete proof of tuslem as of 28-Oct-2024. Lemma for tusbas , tusunif , and tustopn . (Contributed by Thierry Arnoux, 5-Dec-2017) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	tuslem.k	$$⊢K=\mathrm{toUnifSp}\left(U\right)$$
Assertion	tuslemOLD	$$⊢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		1re	$$⊢1\in ℝ$$
4		1lt9	$$⊢1<9$$
5	3 4	ltneii	$$⊢1\ne 9$$
6		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
7		tsetndx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)=9$$
8	6 7	neeq12i	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)\leftrightarrow 1\ne 9$$
9	5 8	mpbir	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
10	2 9	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)}$$
11		ustbas2	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to X=\mathrm{dom}\bigcup U$$
12		uniexg	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \bigcup U\in \mathrm{V}$$
13		dmexg	$$⊢\bigcup U\in \mathrm{V}\to \mathrm{dom}\bigcup U\in \mathrm{V}$$
14		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\}$$
15		df-unif	$$⊢\mathrm{UnifSet}=\mathrm{Slot}13$$
16		1nn	$$⊢1\in \mathbb{N}$$
17		3nn0	$$⊢3\in {\mathbb{N}}_0$$
18		1nn0	$$⊢1\in {\mathbb{N}}_0$$
19		1lt10	$$⊢1<10$$
20	16 17 18 19	declti	$$⊢1<13$$
21		3nn	$$⊢3\in \mathbb{N}$$
22	18 21	decnncl	$$⊢13\in \mathbb{N}$$
23	14 15 20 22	2strbas	$$⊢\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\}}$$
24	12 13 23	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\}}$$
25	11 24	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\}}$$
26		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)⟩$$
27	1 26	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)⟩$$
28	27	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)}$$
29	10 25 28	3eqtr4a	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to X={\mathrm{Base}}_K$$
30		unifid	$$⊢\mathrm{UnifSet}=\mathrm{Slot}\mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
31		9re	$$⊢9\in ℝ$$
32		9nn0	$$⊢9\in {\mathbb{N}}_0$$
33		9lt10	$$⊢9<10$$
34	16 17 32 33	declti	$$⊢9<13$$
35	31 34	gtneii	$$⊢13\ne 9$$
36		unifndx	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)=13$$
37	36 7	neeq12i	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)\leftrightarrow 13\ne 9$$
38	35 37	mpbir	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
39	30 38	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)$$
40	14 15 20 22	2strop	$$⊢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)$$
41	27	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)$$
42	39 40 41	3eqtr4a	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to U=\mathrm{UnifSet}\left(K\right)$$
43		prex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{dom}\bigcup U⟩,⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),U⟩\right\}\in \mathrm{V}$$
44		fvex	$$⊢\mathrm{unifTop}\left(U\right)\in \mathrm{V}$$
45		tsetid	$$⊢\mathrm{TopSet}=\mathrm{Slot}\mathrm{TopSet}\left(\mathrm{ndx}\right)$$
46	45	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)$$
47	43 44 46	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)$$
48	27	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)$$
49	47 48	eqtr4id	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \mathrm{unifTop}\left(U\right)=\mathrm{TopSet}\left(K\right)$$
50		utopbas	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to X=\bigcup \mathrm{unifTop}\left(U\right)$$
51	49	unieqd	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \bigcup \mathrm{unifTop}\left(U\right)=\bigcup \mathrm{TopSet}\left(K\right)$$
52	50 29 51	3eqtr3rd	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \bigcup \mathrm{TopSet}\left(K\right)={\mathrm{Base}}_K$$
53	52	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$$
54		fvex	$$⊢\mathrm{TopSet}\left(K\right)\in \mathrm{V}$$
55		eqid	$$⊢\bigcup \mathrm{TopSet}\left(K\right)=\bigcup \mathrm{TopSet}\left(K\right)$$
56	55	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)$$
57	54 56	ax-mp	$$⊢\mathrm{TopSet}\left(K\right){\upharpoonright }_{𝑡}\bigcup \mathrm{TopSet}\left(K\right)=\mathrm{TopSet}\left(K\right)$$
58		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
59		eqid	$$⊢\mathrm{TopSet}\left(K\right)=\mathrm{TopSet}\left(K\right)$$
60	58 59	topnval	$$⊢\mathrm{TopSet}\left(K\right){\upharpoonright }_{𝑡}{\mathrm{Base}}_K=\mathrm{TopOpen}\left(K\right)$$
61	53 57 60	3eqtr3g	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \mathrm{TopSet}\left(K\right)=\mathrm{TopOpen}\left(K\right)$$
62	49 61	eqtrd	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \mathrm{unifTop}\left(U\right)=\mathrm{TopOpen}\left(K\right)$$
63	29 42 62	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)$$