Metamath Proof Explorer


Theorem utopreg

Description: All Hausdorff uniform spaces are regular. Proposition 3 of BourbakiTop1 p. II.5. (Contributed by Thierry Arnoux, 16-Jan-2018)

Ref Expression
Hypothesis utopreg.1 𝐽 = ( unifTop ‘ 𝑈 )
Assertion utopreg ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) → 𝐽 ∈ Reg )

Proof

Step Hyp Ref Expression
1 utopreg.1 𝐽 = ( unifTop ‘ 𝑈 )
2 utoptop ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) ∈ Top )
3 2 adantr ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) → ( unifTop ‘ 𝑈 ) ∈ Top )
4 1 3 eqeltrid ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) → 𝐽 ∈ Top )
5 simp-4l ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) )
6 4 ad2antrr ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) → 𝐽 ∈ Top )
7 5 6 syl ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → 𝐽 ∈ Top )
8 simplr ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → 𝑤𝑈 )
9 simp-4l ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑤𝑈 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
10 simpr ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑤𝑈 ) → 𝑤𝑈 )
11 4 ad3antrrr ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑤𝑈 ) → 𝐽 ∈ Top )
12 simpllr ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑤𝑈 ) → 𝑎𝐽 )
13 eqid 𝐽 = 𝐽
14 13 eltopss ( ( 𝐽 ∈ Top ∧ 𝑎𝐽 ) → 𝑎 𝐽 )
15 11 12 14 syl2anc ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑤𝑈 ) → 𝑎 𝐽 )
16 utopbas ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = ( unifTop ‘ 𝑈 ) )
17 1 unieqi 𝐽 = ( unifTop ‘ 𝑈 )
18 16 17 eqtr4di ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = 𝐽 )
19 9 18 syl ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑤𝑈 ) → 𝑋 = 𝐽 )
20 15 19 sseqtrrd ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑤𝑈 ) → 𝑎𝑋 )
21 simplr ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑤𝑈 ) → 𝑥𝑎 )
22 20 21 sseldd ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑤𝑈 ) → 𝑥𝑋 )
23 1 utopsnnei ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑤𝑈𝑥𝑋 ) → ( 𝑤 “ { 𝑥 } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
24 9 10 22 23 syl3anc ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑤𝑈 ) → ( 𝑤 “ { 𝑥 } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
25 5 8 24 syl2anc ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → ( 𝑤 “ { 𝑥 } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
26 neii2 ( ( 𝐽 ∈ Top ∧ ( 𝑤 “ { 𝑥 } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ) → ∃ 𝑏𝐽 ( { 𝑥 } ⊆ 𝑏𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) )
27 7 25 26 syl2anc ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → ∃ 𝑏𝐽 ( { 𝑥 } ⊆ 𝑏𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) )
28 simprl ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) ∧ 𝑏𝐽 ) ∧ ( { 𝑥 } ⊆ 𝑏𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) ) → { 𝑥 } ⊆ 𝑏 )
29 vex 𝑥 ∈ V
30 29 snss ( 𝑥𝑏 ↔ { 𝑥 } ⊆ 𝑏 )
31 28 30 sylibr ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) ∧ 𝑏𝐽 ) ∧ ( { 𝑥 } ⊆ 𝑏𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) ) → 𝑥𝑏 )
32 7 ad2antrr ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) ∧ 𝑏𝐽 ) ∧ ( { 𝑥 } ⊆ 𝑏𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) ) → 𝐽 ∈ Top )
33 simplll ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
34 5 33 syl ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
35 34 ad2antrr ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) ∧ 𝑏𝐽 ) ∧ ( { 𝑥 } ⊆ 𝑏𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
36 8 ad2antrr ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) ∧ 𝑏𝐽 ) ∧ ( { 𝑥 } ⊆ 𝑏𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) ) → 𝑤𝑈 )
37 simplr ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) → 𝑎𝐽 )
38 6 37 14 syl2anc ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) → 𝑎 𝐽 )
39 33 18 syl ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) → 𝑋 = 𝐽 )
40 38 39 sseqtrrd ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) → 𝑎𝑋 )
41 simpr ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) → 𝑥𝑎 )
42 40 41 sseldd ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) → 𝑥𝑋 )
43 42 ad6antr ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) ∧ 𝑏𝐽 ) ∧ ( { 𝑥 } ⊆ 𝑏𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) ) → 𝑥𝑋 )
44 ustimasn ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑤𝑈𝑥𝑋 ) → ( 𝑤 “ { 𝑥 } ) ⊆ 𝑋 )
45 35 36 43 44 syl3anc ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) ∧ 𝑏𝐽 ) ∧ ( { 𝑥 } ⊆ 𝑏𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) ) → ( 𝑤 “ { 𝑥 } ) ⊆ 𝑋 )
46 35 18 syl ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) ∧ 𝑏𝐽 ) ∧ ( { 𝑥 } ⊆ 𝑏𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) ) → 𝑋 = 𝐽 )
47 45 46 sseqtrd ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) ∧ 𝑏𝐽 ) ∧ ( { 𝑥 } ⊆ 𝑏𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) ) → ( 𝑤 “ { 𝑥 } ) ⊆ 𝐽 )
48 simprr ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) ∧ 𝑏𝐽 ) ∧ ( { 𝑥 } ⊆ 𝑏𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) ) → 𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) )
49 13 clsss ( ( 𝐽 ∈ Top ∧ ( 𝑤 “ { 𝑥 } ) ⊆ 𝐽𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑏 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑤 “ { 𝑥 } ) ) )
50 32 47 48 49 syl3anc ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) ∧ 𝑏𝐽 ) ∧ ( { 𝑥 } ⊆ 𝑏𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑏 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑤 “ { 𝑥 } ) ) )
51 ustssxp ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑤𝑈 ) → 𝑤 ⊆ ( 𝑋 × 𝑋 ) )
52 34 8 51 syl2anc ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → 𝑤 ⊆ ( 𝑋 × 𝑋 ) )
53 34 18 syl ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → 𝑋 = 𝐽 )
54 53 sqxpeqd ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → ( 𝑋 × 𝑋 ) = ( 𝐽 × 𝐽 ) )
55 52 54 sseqtrd ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → 𝑤 ⊆ ( 𝐽 × 𝐽 ) )
56 5 38 syl ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → 𝑎 𝐽 )
57 simp-5r ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → 𝑥𝑎 )
58 56 57 sseldd ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → 𝑥 𝐽 )
59 13 13 imasncls ( ( ( 𝐽 ∈ Top ∧ 𝐽 ∈ Top ) ∧ ( 𝑤 ⊆ ( 𝐽 × 𝐽 ) ∧ 𝑥 𝐽 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑤 “ { 𝑥 } ) ) ⊆ ( ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑤 ) “ { 𝑥 } ) )
60 7 7 55 58 59 syl22anc ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑤 “ { 𝑥 } ) ) ⊆ ( ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑤 ) “ { 𝑥 } ) )
61 simprl ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → 𝑤 = 𝑤 )
62 1 utop3cls ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑤 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑤𝑈 𝑤 = 𝑤 ) ) → ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑤 ) ⊆ ( 𝑤 ∘ ( 𝑤𝑤 ) ) )
63 34 52 8 61 62 syl22anc ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑤 ) ⊆ ( 𝑤 ∘ ( 𝑤𝑤 ) ) )
64 simprr ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 )
65 63 64 sstrd ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑤 ) ⊆ 𝑣 )
66 imass1 ( ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑤 ) ⊆ 𝑣 → ( ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑤 ) “ { 𝑥 } ) ⊆ ( 𝑣 “ { 𝑥 } ) )
67 65 66 syl ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → ( ( ( cls ‘ ( 𝐽 ×t 𝐽 ) ) ‘ 𝑤 ) “ { 𝑥 } ) ⊆ ( 𝑣 “ { 𝑥 } ) )
68 60 67 sstrd ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑤 “ { 𝑥 } ) ) ⊆ ( 𝑣 “ { 𝑥 } ) )
69 68 ad2antrr ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) ∧ 𝑏𝐽 ) ∧ ( { 𝑥 } ⊆ 𝑏𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑤 “ { 𝑥 } ) ) ⊆ ( 𝑣 “ { 𝑥 } ) )
70 50 69 sstrd ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) ∧ 𝑏𝐽 ) ∧ ( { 𝑥 } ⊆ 𝑏𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑏 ) ⊆ ( 𝑣 “ { 𝑥 } ) )
71 simp-5r ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) ∧ 𝑏𝐽 ) ∧ ( { 𝑥 } ⊆ 𝑏𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) ) → 𝑎 = ( 𝑣 “ { 𝑥 } ) )
72 70 71 sseqtrrd ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) ∧ 𝑏𝐽 ) ∧ ( { 𝑥 } ⊆ 𝑏𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑏 ) ⊆ 𝑎 )
73 31 72 jca ( ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) ∧ 𝑏𝐽 ) ∧ ( { 𝑥 } ⊆ 𝑏𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) ) → ( 𝑥𝑏 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑏 ) ⊆ 𝑎 ) )
74 73 ex ( ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) ∧ 𝑏𝐽 ) → ( ( { 𝑥 } ⊆ 𝑏𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) → ( 𝑥𝑏 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑏 ) ⊆ 𝑎 ) ) )
75 74 reximdva ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → ( ∃ 𝑏𝐽 ( { 𝑥 } ⊆ 𝑏𝑏 ⊆ ( 𝑤 “ { 𝑥 } ) ) → ∃ 𝑏𝐽 ( 𝑥𝑏 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑏 ) ⊆ 𝑎 ) ) )
76 27 75 mpd ( ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) ) → ∃ 𝑏𝐽 ( 𝑥𝑏 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑏 ) ⊆ 𝑎 ) )
77 simp-5l ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
78 simplr ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) → 𝑣𝑈 )
79 ustex3sym ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑣𝑈 ) → ∃ 𝑤𝑈 ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) )
80 77 78 79 syl2anc ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) → ∃ 𝑤𝑈 ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑣 ) )
81 76 80 r19.29a ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) ∧ 𝑣𝑈 ) ∧ 𝑎 = ( 𝑣 “ { 𝑥 } ) ) → ∃ 𝑏𝐽 ( 𝑥𝑏 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑏 ) ⊆ 𝑎 ) )
82 opnneip ( ( 𝐽 ∈ Top ∧ 𝑎𝐽𝑥𝑎 ) → 𝑎 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
83 6 37 41 82 syl3anc ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) → 𝑎 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) )
84 1 utopsnneip ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) = ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑥 } ) ) )
85 33 42 84 syl2anc ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) = ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑥 } ) ) )
86 83 85 eleqtrd ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) → 𝑎 ∈ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑥 } ) ) )
87 eqid ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑥 } ) ) = ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑥 } ) )
88 87 elrnmpt ( 𝑎𝐽 → ( 𝑎 ∈ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑥 } ) ) ↔ ∃ 𝑣𝑈 𝑎 = ( 𝑣 “ { 𝑥 } ) ) )
89 37 88 syl ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) → ( 𝑎 ∈ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑥 } ) ) ↔ ∃ 𝑣𝑈 𝑎 = ( 𝑣 “ { 𝑥 } ) ) )
90 86 89 mpbid ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) → ∃ 𝑣𝑈 𝑎 = ( 𝑣 “ { 𝑥 } ) )
91 81 90 r19.29a ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) ∧ 𝑥𝑎 ) → ∃ 𝑏𝐽 ( 𝑥𝑏 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑏 ) ⊆ 𝑎 ) )
92 91 ralrimiva ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) ∧ 𝑎𝐽 ) → ∀ 𝑥𝑎𝑏𝐽 ( 𝑥𝑏 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑏 ) ⊆ 𝑎 ) )
93 92 ralrimiva ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) → ∀ 𝑎𝐽𝑥𝑎𝑏𝐽 ( 𝑥𝑏 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑏 ) ⊆ 𝑎 ) )
94 isreg ( 𝐽 ∈ Reg ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑎𝐽𝑥𝑎𝑏𝐽 ( 𝑥𝑏 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑏 ) ⊆ 𝑎 ) ) )
95 4 93 94 sylanbrc ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 ∈ Haus ) → 𝐽 ∈ Reg )