Metamath Proof Explorer

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 = 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 tsetndxnbasendx ⊢ TopSet ⁡ ndx ≠ Base ndx
4 3 necomi ⊢ Base ndx ≠ TopSet ⁡ ndx
5 2 4 setsnid ⊢ Base Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U = Base Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U
6 ustbas2 ⊢ U ∈ UnifOn ⁡ X → X = dom ⁡ ⋃ U
7 uniexg ⊢ U ∈ UnifOn ⁡ X → ⋃ U ∈ V
8 dmexg ⊢ ⋃ U ∈ V → dom ⁡ ⋃ U ∈ V
9 eqid ⊢ Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U = Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U
10 basendxltunifndx ⊢ Base ndx < UnifSet ⁡ ndx
11 unifndxnn ⊢ UnifSet ⁡ ndx ∈ ℕ
12 9 10 11 2strbas1 ⊢ dom ⁡ ⋃ U ∈ V → dom ⁡ ⋃ U = Base Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U
13 7 8 12 3syl ⊢ U ∈ UnifOn ⁡ X → dom ⁡ ⋃ U = Base Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U
14 6 13 eqtrd ⊢ U ∈ UnifOn ⁡ X → X = Base Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U
15 tusval ⊢ U ∈ UnifOn ⁡ X → toUnifSp ⁡ U = Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U
16 1 15 eqtrid ⊢ U ∈ UnifOn ⁡ X → K = Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U
17 16 fveq2d ⊢ U ∈ UnifOn ⁡ X → Base K = Base Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U
18 5 14 17 3eqtr4a ⊢ U ∈ UnifOn ⁡ X → X = Base K
19 unifid ⊢ UnifSet = Slot UnifSet ⁡ ndx
20 unifndxntsetndx ⊢ UnifSet ⁡ ndx ≠ TopSet ⁡ ndx
21 19 20 setsnid ⊢ UnifSet ⁡ Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U = UnifSet ⁡ Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U
22 9 10 11 19 2strop1 ⊢ U ∈ UnifOn ⁡ X → U = UnifSet ⁡ Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U
23 16 fveq2d ⊢ U ∈ UnifOn ⁡ X → UnifSet ⁡ K = UnifSet ⁡ Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U
24 21 22 23 3eqtr4a ⊢ U ∈ UnifOn ⁡ X → U = UnifSet ⁡ K
25 prex ⊢ Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U ∈ V
26 fvex ⊢ unifTop ⁡ U ∈ V
27 tsetid ⊢ TopSet = Slot TopSet ⁡ ndx
28 27 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
29 25 26 28 mp2an ⊢ unifTop ⁡ U = TopSet ⁡ Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U
30 16 fveq2d ⊢ U ∈ UnifOn ⁡ X → TopSet ⁡ K = TopSet ⁡ Base ndx dom ⁡ ⋃ U UnifSet ⁡ ndx U sSet TopSet ⁡ ndx unifTop ⁡ U
31 29 30 eqtr4id ⊢ U ∈ UnifOn ⁡ X → unifTop ⁡ U = TopSet ⁡ K
32 utopbas ⊢ U ∈ UnifOn ⁡ X → X = ⋃ unifTop ⁡ U
33 31 unieqd ⊢ U ∈ UnifOn ⁡ X → ⋃ unifTop ⁡ U = ⋃ TopSet ⁡ K
34 32 18 33 3eqtr3rd ⊢ U ∈ UnifOn ⁡ X → ⋃ TopSet ⁡ K = Base K
35 34 oveq2d ⊢ U ∈ UnifOn ⁡ X → TopSet ⁡ K ↾ 𝑡 ⋃ TopSet ⁡ K = TopSet ⁡ K ↾ 𝑡 Base K
36 fvex ⊢ TopSet ⁡ K ∈ V
37 eqid ⊢ ⋃ TopSet ⁡ K = ⋃ TopSet ⁡ K
38 37 restid ⊢ TopSet ⁡ K ∈ V → TopSet ⁡ K ↾ 𝑡 ⋃ TopSet ⁡ K = TopSet ⁡ K
39 36 38 ax-mp ⊢ TopSet ⁡ K ↾ 𝑡 ⋃ TopSet ⁡ K = TopSet ⁡ K
40 eqid ⊢ Base K = Base K
41 eqid ⊢ TopSet ⁡ K = TopSet ⁡ K
42 40 41 topnval ⊢ TopSet ⁡ K ↾ 𝑡 Base K = TopOpen ⁡ K
43 35 39 42 3eqtr3g ⊢ U ∈ UnifOn ⁡ X → TopSet ⁡ K = TopOpen ⁡ K
44 31 43 eqtrd ⊢ U ∈ UnifOn ⁡ X → unifTop ⁡ U = TopOpen ⁡ K
45 18 24 44 3jca ⊢ U ∈ UnifOn ⁡ X → X = Base K ∧ U = UnifSet ⁡ K ∧ unifTop ⁡ U = TopOpen ⁡ K