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 )