Metamath Proof Explorer

Theorem tuslem

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

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 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 ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } ) = ( Base ‘ ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) )
11 ustbas2 ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = dom ∪ 𝑈 )
12 uniexg ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∪ 𝑈 ∈ V )
13 dmexg ⊢ ( ∪ 𝑈 ∈ V → dom ∪ 𝑈 ∈ V )
14 eqid ⊢ { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } = { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ }
15 df-unif ⊢ UnifSet = Slot 1 3
16 1nn ⊢ 1 ∈ ℕ
17 3nn0 ⊢ 3 ∈ ℕ0
18 1nn0 ⊢ 1 ∈ ℕ0
19 1lt10 ⊢ 1 < 1 0
20 16 17 18 19 declti ⊢ 1 < 1 3
21 3nn ⊢ 3 ∈ ℕ
22 18 21 decnncl ⊢ 1 3 ∈ ℕ
23 14 15 20 22 2strbas ⊢ ( dom ∪ 𝑈 ∈ V → dom ∪ 𝑈 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } ) )
24 12 13 23 3syl ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → dom ∪ 𝑈 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } ) )
25 11 24 eqtrd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } ) )
26 tusval ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( toUnifSp ‘ 𝑈 ) = ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) )
27 1 26 syl5eq ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝐾 = ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) )
28 27 fveq2d ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( Base ‘ 𝐾 ) = ( Base ‘ ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) ) )
29 10 25 28 3eqtr4a ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = ( Base ‘ 𝐾 ) )
30 unifid ⊢ UnifSet = Slot ( UnifSet ‘ ndx )
31 9re ⊢ 9 ∈ ℝ
32 9nn0 ⊢ 9 ∈ ℕ0
33 9lt10 ⊢ 9 < 1 0
34 16 17 32 33 declti ⊢ 9 < 1 3
35 31 34 gtneii ⊢ 1 3 ≠ 9
36 unifndx ⊢ ( UnifSet ‘ ndx ) = 1 3
37 36 7 neeq12i ⊢ ( ( UnifSet ‘ ndx ) ≠ ( TopSet ‘ ndx ) ↔ 1 3 ≠ 9 )
38 35 37 mpbir ⊢ ( UnifSet ‘ ndx ) ≠ ( TopSet ‘ ndx )
39 30 38 setsnid ⊢ ( UnifSet ‘ { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } ) = ( UnifSet ‘ ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) )
40 14 15 20 22 2strop ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 = ( UnifSet ‘ { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } ) )
41 27 fveq2d ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( UnifSet ‘ 𝐾 ) = ( UnifSet ‘ ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) ) )
42 39 40 41 3eqtr4a ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 = ( UnifSet ‘ 𝐾 ) )
43 prex ⊢ { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } ∈ V
44 fvex ⊢ ( unifTop ‘ 𝑈 ) ∈ V
45 tsetid ⊢ TopSet = Slot ( TopSet ‘ ndx )
46 45 setsid ⊢ ( ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } ∈ V ∧ ( unifTop ‘ 𝑈 ) ∈ V ) → ( unifTop ‘ 𝑈 ) = ( TopSet ‘ ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) ) )
47 43 44 46 mp2an ⊢ ( unifTop ‘ 𝑈 ) = ( TopSet ‘ ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) )
48 27 fveq2d ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( TopSet ‘ 𝐾 ) = ( TopSet ‘ ( { ⟨ ( Base ‘ ndx ) , dom ∪ 𝑈 ⟩ , ⟨ ( UnifSet ‘ ndx ) , 𝑈 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) ⟩ ) ) )
49 47 48 eqtr4id ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) = ( TopSet ‘ 𝐾 ) )
50 utopbas ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = ∪ ( unifTop ‘ 𝑈 ) )
51 49 unieqd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∪ ( unifTop ‘ 𝑈 ) = ∪ ( TopSet ‘ 𝐾 ) )
52 50 29 51 3eqtr3rd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∪ ( TopSet ‘ 𝐾 ) = ( Base ‘ 𝐾 ) )
53 52 oveq2d ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ( TopSet ‘ 𝐾 ) ↾t ∪ ( TopSet ‘ 𝐾 ) ) = ( ( TopSet ‘ 𝐾 ) ↾t ( Base ‘ 𝐾 ) ) )
54 fvex ⊢ ( TopSet ‘ 𝐾 ) ∈ V
55 eqid ⊢ ∪ ( TopSet ‘ 𝐾 ) = ∪ ( TopSet ‘ 𝐾 )
56 55 restid ⊢ ( ( TopSet ‘ 𝐾 ) ∈ V → ( ( TopSet ‘ 𝐾 ) ↾t ∪ ( TopSet ‘ 𝐾 ) ) = ( TopSet ‘ 𝐾 ) )
57 54 56 ax-mp ⊢ ( ( TopSet ‘ 𝐾 ) ↾t ∪ ( TopSet ‘ 𝐾 ) ) = ( TopSet ‘ 𝐾 )
58 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
59 eqid ⊢ ( TopSet ‘ 𝐾 ) = ( TopSet ‘ 𝐾 )
60 58 59 topnval ⊢ ( ( TopSet ‘ 𝐾 ) ↾t ( Base ‘ 𝐾 ) ) = ( TopOpen ‘ 𝐾 )
61 53 57 60 3eqtr3g ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( TopSet ‘ 𝐾 ) = ( TopOpen ‘ 𝐾 ) )
62 49 61 eqtrd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) = ( TopOpen ‘ 𝐾 ) )
63 29 42 62 3jca ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑋 = ( Base ‘ 𝐾 ) ∧ 𝑈 = ( UnifSet ‘ 𝐾 ) ∧ ( unifTop ‘ 𝑈 ) = ( TopOpen ‘ 𝐾 ) ) )