Metamath Proof Explorer

Theorem tuslem

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

Ref Expression
Hypothesis tuslem.k ⊢ K = toUnifSp ⁡ U
Assertion tuslem ⊢ U ∈ UnifOn ⁡ X → X = Base K ∧ U = UnifSet ⁡ K ∧ unifTop ⁡ U = TopOpen ⁡ K

Proof

Step Hyp Ref Expression
1 tuslem.k ⊢ K = toUnifSp ⁡ U
2 baseid ⊢ Base = Slot Base ndx
3 1re ⊢ 1 ∈ ℝ
4 1lt9 ⊢ 1 < 9
5 3 4 ltneii ⊢ 1 ≠ 9
6 basendx ⊢ Base ndx = 1
7 tsetndx ⊢ TopSet ⁡ ndx = 9
8 6 7 neeq12i ⊢ Base ndx ≠ TopSet ⁡ ndx ↔ 1 ≠ 9
9 5 8 mpbir ⊢ Base ndx ≠ TopSet ⁡ ndx
10 2 9 setsnid ⊢ Base Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U = Base Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U
11 ustbas2 ⊢ U ∈ UnifOn ⁡ X → X = dom ⁡ ⋃ U
12 uniexg ⊢ U ∈ UnifOn ⁡ X → ⋃ U ∈ V
13 dmexg ⊢ ⋃ U ∈ V → dom ⁡ ⋃ U ∈ V
14 eqid ⊢ Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U = Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U
15 df-unif ⊢ UnifSet = Slot 13
16 1nn ⊢ 1 ∈ ℕ
17 3nn0 ⊢ 3 ∈ ℕ 0
18 1nn0 ⊢ 1 ∈ ℕ 0
19 1lt10 ⊢ 1 < 10
20 16 17 18 19 declti ⊢ 1 < 13
21 3nn ⊢ 3 ∈ ℕ
22 18 21 decnncl ⊢ 13 ∈ ℕ
23 14 15 20 22 2strbas ⊢ dom ⁡ ⋃ U ∈ V → dom ⁡ ⋃ U = Base Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U
24 12 13 23 3syl ⊢ U ∈ UnifOn ⁡ X → dom ⁡ ⋃ U = Base Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U
25 11 24 eqtrd ⊢ U ∈ UnifOn ⁡ X → X = Base Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U
26 tusval ⊢ U ∈ UnifOn ⁡ X → toUnifSp ⁡ U = Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U
27 1 26 syl5eq ⊢ U ∈ UnifOn ⁡ X → K = Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U
28 27 fveq2d ⊢ U ∈ UnifOn ⁡ X → Base K = Base Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U
29 10 25 28 3eqtr4a ⊢ U ∈ UnifOn ⁡ X → X = Base K
30 unifid ⊢ UnifSet = Slot UnifSet ⁡ ndx
31 9re ⊢ 9 ∈ ℝ
32 9nn0 ⊢ 9 ∈ ℕ 0
33 9lt10 ⊢ 9 < 10
34 16 17 32 33 declti ⊢ 9 < 13
35 31 34 gtneii ⊢ 13 ≠ 9
36 unifndx ⊢ UnifSet ⁡ ndx = 13
37 36 7 neeq12i ⊢ UnifSet ⁡ ndx ≠ TopSet ⁡ ndx ↔ 13 ≠ 9
38 35 37 mpbir ⊢ UnifSet ⁡ ndx ≠ TopSet ⁡ ndx
39 30 38 setsnid ⊢ UnifSet ⁡ Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U = UnifSet ⁡ Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U
40 14 15 20 22 2strop ⊢ U ∈ UnifOn ⁡ X → U = UnifSet ⁡ Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U
41 27 fveq2d ⊢ U ∈ UnifOn ⁡ X → UnifSet ⁡ K = UnifSet ⁡ Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U
42 39 40 41 3eqtr4a ⊢ U ∈ UnifOn ⁡ X → U = UnifSet ⁡ K
43 prex ⊢ Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U ∈ V
44 fvex ⊢ unifTop ⁡ U ∈ V
45 tsetid ⊢ TopSet = Slot TopSet ⁡ ndx
46 45 setsid ⊢ Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U ∈ V ∧ unifTop ⁡ U ∈ V → unifTop ⁡ U = TopSet ⁡ Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U
47 43 44 46 mp2an ⊢ unifTop ⁡ U = TopSet ⁡ Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U
48 27 fveq2d ⊢ U ∈ UnifOn ⁡ X → TopSet ⁡ K = TopSet ⁡ Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U
49 47 48 eqtr4id ⊢ U ∈ UnifOn ⁡ X → unifTop ⁡ U = TopSet ⁡ K
50 utopbas ⊢ U ∈ UnifOn ⁡ X → X = ⋃ unifTop ⁡ U
51 49 unieqd ⊢ U ∈ UnifOn ⁡ X → ⋃ unifTop ⁡ U = ⋃ TopSet ⁡ K
52 50 29 51 3eqtr3rd ⊢ U ∈ UnifOn ⁡ X → ⋃ TopSet ⁡ K = Base K
53 52 oveq2d ⊢ U ∈ UnifOn ⁡ X → TopSet ⁡ K ↾ 𝑡 ⋃ TopSet ⁡ K = TopSet ⁡ K ↾ 𝑡 Base K
54 fvex ⊢ TopSet ⁡ K ∈ V
55 eqid ⊢ ⋃ TopSet ⁡ K = ⋃ TopSet ⁡ K
56 55 restid ⊢ TopSet ⁡ K ∈ V → TopSet ⁡ K ↾ 𝑡 ⋃ TopSet ⁡ K = TopSet ⁡ K
57 54 56 ax-mp ⊢ TopSet ⁡ K ↾ 𝑡 ⋃ TopSet ⁡ K = TopSet ⁡ K
58 eqid ⊢ Base K = Base K
59 eqid ⊢ TopSet ⁡ K = TopSet ⁡ K
60 58 59 topnval ⊢ TopSet ⁡ K ↾ 𝑡 Base K = TopOpen ⁡ K
61 53 57 60 3eqtr3g ⊢ U ∈ UnifOn ⁡ X → TopSet ⁡ K = TopOpen ⁡ K
62 49 61 eqtrd ⊢ U ∈ UnifOn ⁡ X → unifTop ⁡ U = TopOpen ⁡ K
63 29 42 62 3jca ⊢ U ∈ UnifOn ⁡ X → X = Base K ∧ U = UnifSet ⁡ K ∧ unifTop ⁡ U = TopOpen ⁡ K