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 ⊢ 𝐾 = ( toUnifSp ‘ 𝑈 )
Assertion tuslem ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑋 = ( Base ‘ 𝐾 ) ∧ 𝑈 = ( UnifSet ‘ 𝐾 ) ∧ ( unifTop ‘ 𝑈 ) = ( TopOpen ‘ 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 tuslem.k ⊢ 𝐾 = ( toUnifSp ‘ 𝑈 )
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 ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } ) = ( Base ‘ ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) )
6 ustbas2 ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = dom ∪ 𝑈 )
7 uniexg ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∪ 𝑈 ∈ V )
8 dmexg ⊢ ( ∪ 𝑈 ∈ V → dom ∪ 𝑈 ∈ V )
9 eqid ⊢ { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } = { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ }
10 basendxltunifndx ⊢ ( Base ‘ ndx ) < ( UnifSet ‘ ndx )
11 unifndxnn ⊢ ( UnifSet ‘ ndx ) ∈ ℕ
12 9 10 11 2strbas1 ⊢ ( dom ∪ 𝑈 ∈ V → dom ∪ 𝑈 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } ) )
13 7 8 12 3syl ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → dom ∪ 𝑈 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } ) )
14 6 13 eqtrd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } ) )
15 tusval ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( toUnifSp ‘ 𝑈 ) = ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) )
16 1 15 eqtrid ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝐾 = ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) )
17 16 fveq2d ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( Base ‘ 𝐾 ) = ( Base ‘ ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) ) )
18 5 14 17 3eqtr4a ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = ( Base ‘ 𝐾 ) )
19 unifid ⊢ UnifSet = Slot ( UnifSet ‘ ndx )
20 unifndxntsetndx ⊢ ( UnifSet ‘ ndx ) ≠ ( TopSet ‘ ndx )
21 19 20 setsnid ⊢ ( UnifSet ‘ { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } ) = ( UnifSet ‘ ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) )
22 9 10 11 19 2strop1 ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 = ( UnifSet ‘ { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } ) )
23 16 fveq2d ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( UnifSet ‘ 𝐾 ) = ( UnifSet ‘ ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) ) )
24 21 22 23 3eqtr4a ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 = ( UnifSet ‘ 𝐾 ) )
25 prex ⊢ { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } ∈ V
26 fvex ⊢ ( unifTop ‘ 𝑈 ) ∈ V
27 tsetid ⊢ TopSet = Slot ( TopSet ‘ ndx )
28 27 setsid ⊢ ( ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } ∈ V ∧ ( unifTop ‘ 𝑈 ) ∈ V ) → ( unifTop ‘ 𝑈 ) = ( TopSet ‘ ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) ) )
29 25 26 28 mp2an ⊢ ( unifTop ‘ 𝑈 ) = ( TopSet ‘ ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) )
30 16 fveq2d ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( TopSet ‘ 𝐾 ) = ( TopSet ‘ ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) ) )
31 29 30 eqtr4id ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) = ( TopSet ‘ 𝐾 ) )
32 utopbas ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = ∪ ( unifTop ‘ 𝑈 ) )
33 31 unieqd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∪ ( unifTop ‘ 𝑈 ) = ∪ ( TopSet ‘ 𝐾 ) )
34 32 18 33 3eqtr3rd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∪ ( TopSet ‘ 𝐾 ) = ( Base ‘ 𝐾 ) )
35 34 oveq2d ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ( TopSet ‘ 𝐾 ) ↾t ∪ ( TopSet ‘ 𝐾 ) ) = ( ( TopSet ‘ 𝐾 ) ↾t ( Base ‘ 𝐾 ) ) )
36 fvex ⊢ ( TopSet ‘ 𝐾 ) ∈ V
37 eqid ⊢ ∪ ( TopSet ‘ 𝐾 ) = ∪ ( TopSet ‘ 𝐾 )
38 37 restid ⊢ ( ( TopSet ‘ 𝐾 ) ∈ V → ( ( TopSet ‘ 𝐾 ) ↾t ∪ ( TopSet ‘ 𝐾 ) ) = ( TopSet ‘ 𝐾 ) )
39 36 38 ax-mp ⊢ ( ( TopSet ‘ 𝐾 ) ↾t ∪ ( TopSet ‘ 𝐾 ) ) = ( TopSet ‘ 𝐾 )
40 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
41 eqid ⊢ ( TopSet ‘ 𝐾 ) = ( TopSet ‘ 𝐾 )
42 40 41 topnval ⊢ ( ( TopSet ‘ 𝐾 ) ↾t ( Base ‘ 𝐾 ) ) = ( TopOpen ‘ 𝐾 )
43 35 39 42 3eqtr3g ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( TopSet ‘ 𝐾 ) = ( TopOpen ‘ 𝐾 ) )
44 31 43 eqtrd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) = ( TopOpen ‘ 𝐾 ) )
45 18 24 44 3jca ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑋 = ( Base ‘ 𝐾 ) ∧ 𝑈 = ( UnifSet ‘ 𝐾 ) ∧ ( unifTop ‘ 𝑈 ) = ( TopOpen ‘ 𝐾 ) ) )