Theorem tuslemOLD 24190

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

Hypothesis

Ref	Expression
tuslem.k	⊢ 𝐾 = (toUnifSp‘𝑈)

Assertion

Ref	Expression
tuslemOLD	⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 = (Base‘𝐾) ∧ 𝑈 = (UnifSet‘𝐾) ∧ (unifTop‘𝑈) = (TopOpen‘𝐾)))

Proof of Theorem tuslemOLD

Step	Hyp	Ref	Expression
1		baseid 17182	. . . 4 ⊢ Base = Slot (Base‘ndx)
2		1re 11244	. . . . . 6 ⊢ 1 ∈ ℝ
3		1lt9 12448	. . . . . 6 ⊢ 1 < 9
4	2, 3	ltneii 11357	. . . . 5 ⊢ 1 ≠ 9
5		basendx 17188	. . . . . 6 ⊢ (Base‘ndx) = 1
6		tsetndx 17332	. . . . . 6 ⊢ (TopSet‘ndx) = 9
7	5, 6	neeq12i 2997	. . . . 5 ⊢ ((Base‘ndx) ≠ (TopSet‘ndx) ↔ 1 ≠ 9)
8	4, 7	mpbir 230	. . . 4 ⊢ (Base‘ndx) ≠ (TopSet‘ndx)
9	1, 8	setsnid 17177	. . 3 ⊢ (Base‘{⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩}) = (Base‘({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩))
10		ustbas2 24148	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = dom ∪ 𝑈)
11		uniexg 7743	. . . . 5 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ 𝑈 ∈ V)
12		dmexg 7907	. . . . 5 ⊢ (∪ 𝑈 ∈ V → dom ∪ 𝑈 ∈ V)
13		eqid 2725	. . . . . 6 ⊢ {⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} = {⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩}
14		df-unif 17255	. . . . . 6 ⊢ UnifSet = Slot ;13
15		1nn 12253	. . . . . . 7 ⊢ 1 ∈ ℕ
16		3nn0 12520	. . . . . . 7 ⊢ 3 ∈ ℕ0
17		1nn0 12518	. . . . . . 7 ⊢ 1 ∈ ℕ0
18		1lt10 12846	. . . . . . 7 ⊢ 1 < ;10
19	15, 16, 17, 18	declti 12745	. . . . . 6 ⊢ 1 < ;13
20		3nn 12321	. . . . . . 7 ⊢ 3 ∈ ℕ
21	17, 20	decnncl 12727	. . . . . 6 ⊢ ;13 ∈ ℕ
22	13, 14, 19, 21	2strbas 17202	. . . . 5 ⊢ (dom ∪ 𝑈 ∈ V → dom ∪ 𝑈 = (Base‘{⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩}))
23	11, 12, 22	3syl 18	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → dom ∪ 𝑈 = (Base‘{⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩}))
24	10, 23	eqtrd 2765	. . 3 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = (Base‘{⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩}))
25		tuslem.k	. . . . 5 ⊢ 𝐾 = (toUnifSp‘𝑈)
26		tusval 24188	. . . . 5 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (toUnifSp‘𝑈) = ({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩))
27	25, 26	eqtrid 2777	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 = ({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩))
28	27	fveq2d 6896	. . 3 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (Base‘𝐾) = (Base‘({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩)))
29	9, 24, 28	3eqtr4a 2791	. 2 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = (Base‘𝐾))
30		unifid 17376	. . . 4 ⊢ UnifSet = Slot (UnifSet‘ndx)
31		9re 12341	. . . . . 6 ⊢ 9 ∈ ℝ
32		9nn0 12526	. . . . . . 7 ⊢ 9 ∈ ℕ0
33		9lt10 12838	. . . . . . 7 ⊢ 9 < ;10
34	15, 16, 32, 33	declti 12745	. . . . . 6 ⊢ 9 < ;13
35	31, 34	gtneii 11356	. . . . 5 ⊢ ;13 ≠ 9
36		unifndx 17375	. . . . . 6 ⊢ (UnifSet‘ndx) = ;13
37	36, 6	neeq12i 2997	. . . . 5 ⊢ ((UnifSet‘ndx) ≠ (TopSet‘ndx) ↔ ;13 ≠ 9)
38	35, 37	mpbir 230	. . . 4 ⊢ (UnifSet‘ndx) ≠ (TopSet‘ndx)
39	30, 38	setsnid 17177	. . 3 ⊢ (UnifSet‘{⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩}) = (UnifSet‘({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩))
40	13, 14, 19, 21	2strop 17203	. . 3 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSet‘{⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩}))
41	27	fveq2d 6896	. . 3 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (UnifSet‘𝐾) = (UnifSet‘({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩)))
42	39, 40, 41	3eqtr4a 2791	. 2 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSet‘𝐾))
43		prex 5428	. . . . 5 ⊢ {⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} ∈ V
44		fvex 6905	. . . . 5 ⊢ (unifTop‘𝑈) ∈ V
45		tsetid 17333	. . . . . 6 ⊢ TopSet = Slot (TopSet‘ndx)
46	45	setsid 17176	. . . . 5 ⊢ (({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} ∈ V ∧ (unifTop‘𝑈) ∈ V) → (unifTop‘𝑈) = (TopSet‘({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩)))
47	43, 44, 46	mp2an 690	. . . 4 ⊢ (unifTop‘𝑈) = (TopSet‘({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩))
48	27	fveq2d 6896	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (TopSet‘𝐾) = (TopSet‘({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩)))
49	47, 48	eqtr4id 2784	. . 3 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = (TopSet‘𝐾))
50		utopbas 24158	. . . . . 6 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = ∪ (unifTop‘𝑈))
51	49	unieqd 4916	. . . . . 6 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ (unifTop‘𝑈) = ∪ (TopSet‘𝐾))
52	50, 29, 51	3eqtr3rd 2774	. . . . 5 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ (TopSet‘𝐾) = (Base‘𝐾))
53	52	oveq2d 7432	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ((TopSet‘𝐾) ↾t ∪ (TopSet‘𝐾)) = ((TopSet‘𝐾) ↾t (Base‘𝐾)))
54		fvex 6905	. . . . 5 ⊢ (TopSet‘𝐾) ∈ V
55		eqid 2725	. . . . . 6 ⊢ ∪ (TopSet‘𝐾) = ∪ (TopSet‘𝐾)
56	55	restid 17414	. . . . 5 ⊢ ((TopSet‘𝐾) ∈ V → ((TopSet‘𝐾) ↾t ∪ (TopSet‘𝐾)) = (TopSet‘𝐾))
57	54, 56	ax-mp 5	. . . 4 ⊢ ((TopSet‘𝐾) ↾t ∪ (TopSet‘𝐾)) = (TopSet‘𝐾)
58		eqid 2725	. . . . 5 ⊢ (Base‘𝐾) = (Base‘𝐾)
59		eqid 2725	. . . . 5 ⊢ (TopSet‘𝐾) = (TopSet‘𝐾)
60	58, 59	topnval 17415	. . . 4 ⊢ ((TopSet‘𝐾) ↾t (Base‘𝐾)) = (TopOpen‘𝐾)
61	53, 57, 60	3eqtr3g 2788	. . 3 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (TopSet‘𝐾) = (TopOpen‘𝐾))
62	49, 61	eqtrd 2765	. 2 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = (TopOpen‘𝐾))
63	29, 42, 62	3jca 1125	1 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 = (Base‘𝐾) ∧ 𝑈 = (UnifSet‘𝐾) ∧ (unifTop‘𝑈) = (TopOpen‘𝐾)))

Syntax hints:   → wi 4   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   ≠ wne 2930  Vcvv 3463  {cpr 4626  ⟨cop 4630  ∪ cuni 4903  dom cdm 5672  ‘cfv 6543  (class class class)co 7416  1c1 11139  3c3 12298  9c9 12304  ;cdc 12707   sSet csts 17131  ndxcnx 17161  Basecbs 17179  TopSetcts 17238  UnifSetcunif 17242   ↾_t crest 17401  TopOpenctopn 17402  UnifOncust 24122  unifTopcutop 24153  toUnifSpctus 24178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7738  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3769  df-csb 3885  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-pss 3959  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7869  df-1st 7991  df-2nd 7992  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-er 8723  df-en 8963  df-dom 8964  df-sdom 8965  df-fin 8966  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-nn 12243  df-2 12305  df-3 12306  df-4 12307  df-5 12308  df-6 12309  df-7 12310  df-8 12311  df-9 12312  df-n0 12503  df-z 12589  df-dec 12708  df-uz 12853  df-fz 13517  df-struct 17115  df-sets 17132  df-slot 17150  df-ndx 17162  df-base 17180  df-tset 17251  df-unif 17255  df-rest 17403  df-topn 17404  df-ust 24123  df-utop 24154  df-tus 24181

This theorem is referenced by: (None)