tuslem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > tuslem		Structured version Visualization version GIF version

Theorem tuslem 22878

Description: Lemma for tusbas 22879, tusunif 22880, and tustopn 22882. (Contributed by Thierry Arnoux, 5-Dec-2017.)

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

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

**Proof of Theorem tuslem**
Step	Hyp	Ref	Expression
1		baseid 16545	. . . 4 ⊢ Base = Slot (Base‘ndx)
2		1re 10643	. . . . . 6 ⊢ 1 ∈ ℝ
3		1lt9 11846	. . . . . 6 ⊢ 1 < 9
4	2, 3	ltneii 10755	. . . . 5 ⊢ 1 ≠ 9
5		basendx 16549	. . . . . 6 ⊢ (Base‘ndx) = 1
6		tsetndx 16661	. . . . . 6 ⊢ (TopSet‘ndx) = 9
7	5, 6	neeq12i 3084	. . . . 5 ⊢ ((Base‘ndx) ≠ (TopSet‘ndx) ↔ 1 ≠ 9)
8	4, 7	mpbir 233	. . . 4 ⊢ (Base‘ndx) ≠ (TopSet‘ndx)
9	1, 8	setsnid 16541	. . 3 ⊢ (Base‘{⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩}) = (Base‘({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩))
10		ustbas2 22836	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = dom ∪ 𝑈)
11		uniexg 7468	. . . . 5 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ 𝑈 ∈ V)
12		dmexg 7615	. . . . 5 ⊢ (∪ 𝑈 ∈ V → dom ∪ 𝑈 ∈ V)
13		eqid 2823	. . . . . 6 ⊢ {⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} = {⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩}
14		df-unif 16590	. . . . . 6 ⊢ UnifSet = Slot ;13
15		1nn 11651	. . . . . . 7 ⊢ 1 ∈ ℕ
16		3nn0 11918	. . . . . . 7 ⊢ 3 ∈ ℕ₀
17		1nn0 11916	. . . . . . 7 ⊢ 1 ∈ ℕ₀
18		1lt10 12240	. . . . . . 7 ⊢ 1 < ;10
19	15, 16, 17, 18	declti 12139	. . . . . 6 ⊢ 1 < ;13
20		3nn 11719	. . . . . . 7 ⊢ 3 ∈ ℕ
21	17, 20	decnncl 12121	. . . . . 6 ⊢ ;13 ∈ ℕ
22	13, 14, 19, 21	2strbas 16605	. . . . 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 2858	. . 3 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = (Base‘{⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩}))
25		tuslem.k	. . . . 5 ⊢ 𝐾 = (toUnifSp‘𝑈)
26		tusval 22877	. . . . 5 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (toUnifSp‘𝑈) = ({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩))
27	25, 26	syl5eq 2870	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 = ({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩))
28	27	fveq2d 6676	. . 3 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (Base‘𝐾) = (Base‘({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩)))
29	9, 24, 28	3eqtr4a 2884	. 2 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = (Base‘𝐾))
30		unifid 16680	. . . 4 ⊢ UnifSet = Slot (UnifSet‘ndx)
31		9re 11739	. . . . . 6 ⊢ 9 ∈ ℝ
32		9nn0 11924	. . . . . . 7 ⊢ 9 ∈ ℕ₀
33		9lt10 12232	. . . . . . 7 ⊢ 9 < ;10
34	15, 16, 32, 33	declti 12139	. . . . . 6 ⊢ 9 < ;13
35	31, 34	gtneii 10754	. . . . 5 ⊢ ;13 ≠ 9
36		unifndx 16679	. . . . . 6 ⊢ (UnifSet‘ndx) = ;13
37	36, 6	neeq12i 3084	. . . . 5 ⊢ ((UnifSet‘ndx) ≠ (TopSet‘ndx) ↔ ;13 ≠ 9)
38	35, 37	mpbir 233	. . . 4 ⊢ (UnifSet‘ndx) ≠ (TopSet‘ndx)
39	30, 38	setsnid 16541	. . 3 ⊢ (UnifSet‘{⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩}) = (UnifSet‘({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩))
40	13, 14, 19, 21	2strop 16606	. . 3 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSet‘{⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩}))
41	27	fveq2d 6676	. . 3 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (UnifSet‘𝐾) = (UnifSet‘({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩)))
42	39, 40, 41	3eqtr4a 2884	. 2 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSet‘𝐾))
43	27	fveq2d 6676	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (TopSet‘𝐾) = (TopSet‘({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩)))
44		prex 5335	. . . . 5 ⊢ {⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} ∈ V
45		fvex 6685	. . . . 5 ⊢ (unifTop‘𝑈) ∈ V
46		tsetid 16662	. . . . . 6 ⊢ TopSet = Slot (TopSet‘ndx)
47	46	setsid 16540	. . . . 5 ⊢ (({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} ∈ V ∧ (unifTop‘𝑈) ∈ V) → (unifTop‘𝑈) = (TopSet‘({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩)))
48	44, 45, 47	mp2an 690	. . . 4 ⊢ (unifTop‘𝑈) = (TopSet‘({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx), (unifTop‘𝑈)⟩))
49	43, 48	syl6reqr 2877	. . 3 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = (TopSet‘𝐾))
50		utopbas 22846	. . . . . 6 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = ∪ (unifTop‘𝑈))
51	49	unieqd 4854	. . . . . 6 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ (unifTop‘𝑈) = ∪ (TopSet‘𝐾))
52	50, 29, 51	3eqtr3rd 2867	. . . . 5 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ (TopSet‘𝐾) = (Base‘𝐾))
53	52	oveq2d 7174	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → ((TopSet‘𝐾) ↾_t ∪ (TopSet‘𝐾)) = ((TopSet‘𝐾) ↾_t (Base‘𝐾)))
54		fvex 6685	. . . . 5 ⊢ (TopSet‘𝐾) ∈ V
55		eqid 2823	. . . . . 6 ⊢ ∪ (TopSet‘𝐾) = ∪ (TopSet‘𝐾)
56	55	restid 16709	. . . . 5 ⊢ ((TopSet‘𝐾) ∈ V → ((TopSet‘𝐾) ↾_t ∪ (TopSet‘𝐾)) = (TopSet‘𝐾))
57	54, 56	ax-mp 5	. . . 4 ⊢ ((TopSet‘𝐾) ↾_t ∪ (TopSet‘𝐾)) = (TopSet‘𝐾)
58		eqid 2823	. . . . 5 ⊢ (Base‘𝐾) = (Base‘𝐾)
59		eqid 2823	. . . . 5 ⊢ (TopSet‘𝐾) = (TopSet‘𝐾)
60	58, 59	topnval 16710	. . . 4 ⊢ ((TopSet‘𝐾) ↾_t (Base‘𝐾)) = (TopOpen‘𝐾)
61	53, 57, 60	3eqtr3g 2881	. . 3 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (TopSet‘𝐾) = (TopOpen‘𝐾))
62	49, 61	eqtrd 2858	. 2 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = (TopOpen‘𝐾))
63	29, 42, 62	3jca 1124	1 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 = (Base‘𝐾) ∧ 𝑈 = (UnifSet‘𝐾) ∧ (unifTop‘𝑈) = (TopOpen‘𝐾)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 ≠ wne 3018 Vcvv 3496 {cpr 4571 ⟨cop 4575 ∪ cuni 4840 dom cdm 5557 ‘cfv 6357 (class class class)co 7158 1c1 10540 3c3 11696 9c9 11702 cdc 12101 ndxcnx 16482 sSet csts 16483 Basecbs 16485 TopSetcts 16573 UnifSetcunif 16577 ↾_t crest 16696 TopOpenctopn 16697 UnifOncust 22810 unifTopcutop 22841 toUnifSpctus 22866

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-cnex 10595 ax-resscn 10596 ax-1cn 10597 ax-icn 10598 ax-addcl 10599 ax-addrcl 10600 ax-mulcl 10601 ax-mulrcl 10602 ax-mulcom 10603 ax-addass 10604 ax-mulass 10605 ax-distr 10606 ax-i2m1 10607 ax-1ne0 10608 ax-1rid 10609 ax-rnegex 10610 ax-rrecex 10611 ax-cnre 10612 ax-pre-lttri 10613 ax-pre-lttrn 10614 ax-pre-ltadd 10615 ax-pre-mulgt0 10616

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-reu 3147 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-int 4879 df-iun 4923 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-pred 6150 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-riota 7116 df-ov 7161 df-oprab 7162 df-mpo 7163 df-om 7583 df-1st 7691 df-2nd 7692 df-wrecs 7949 df-recs 8010 df-rdg 8048 df-1o 8104 df-oadd 8108 df-er 8291 df-en 8512 df-dom 8513 df-sdom 8514 df-fin 8515 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 df-sub 10874 df-neg 10875 df-nn 11641 df-2 11703 df-3 11704 df-4 11705 df-5 11706 df-6 11707 df-7 11708 df-8 11709 df-9 11710 df-n0 11901 df-z 11985 df-dec 12102 df-uz 12247 df-fz 12896 df-struct 16487 df-ndx 16488 df-slot 16489 df-base 16491 df-sets 16492 df-tset 16586 df-unif 16590 df-rest 16698 df-topn 16699 df-ust 22811 df-utop 22842 df-tus 22869

This theorem is referenced by: tusbas 22879 tusunif 22880 tustopn 22882 tususp 22883

W3C validator