This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem utoptop

Description: The topology induced by a uniform structure U is a topology. (Contributed by Thierry Arnoux, 30-Nov-2017)

Ref Expression
Assertion utoptop ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) ∈ Top )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) → 𝑥 ⊆ ( unifTop ‘ 𝑈 ) )
2 utopval ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑎 } )
3 ssrab2 ⊢ { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑎 } ⊆ 𝒫 𝑋
4 2 3 eqsstrdi ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) ⊆ 𝒫 𝑋 )
5 4 adantr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) → ( unifTop ‘ 𝑈 ) ⊆ 𝒫 𝑋 )
6 1 5 sstrd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) → 𝑥 ⊆ 𝒫 𝑋 )
7 sspwuni ⊢ ( 𝑥 ⊆ 𝒫 𝑋 ↔ ∪ 𝑥 ⊆ 𝑋 )
8 6 7 sylib ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) → ∪ 𝑥 ⊆ 𝑋 )
9 simp-4l ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ∪ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑝 ∈ 𝑦 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
10 simp-4r ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ∪ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑝 ∈ 𝑦 ) → 𝑥 ⊆ ( unifTop ‘ 𝑈 ) )
11 simplr ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ∪ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑝 ∈ 𝑦 ) → 𝑦 ∈ 𝑥 )
12 10 11 sseldd ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ∪ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑝 ∈ 𝑦 ) → 𝑦 ∈ ( unifTop ‘ 𝑈 ) )
13 simpr ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ∪ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑝 ∈ 𝑦 ) → 𝑝 ∈ 𝑦 )
14 elutop ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑦 ∈ ( unifTop ‘ 𝑈 ) ↔ ( 𝑦 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑦 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) )
15 14 biimpa ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) → ( 𝑦 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑦 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) )
16 15 simprd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) → ∀ 𝑝 ∈ 𝑦 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 )
17 16 r19.21bi ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ 𝑦 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 )
18 9 12 13 17 syl21anc ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ∪ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑝 ∈ 𝑦 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 )
19 r19.41v ⊢ ( ∃ 𝑣 ∈ 𝑈 ( ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ∧ 𝑦 ∈ 𝑥 ) ↔ ( ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ∧ 𝑦 ∈ 𝑥 ) )
20 ssuni ⊢ ( ( ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → ( 𝑣 “ { 𝑝 } ) ⊆ ∪ 𝑥 )
21 20 reximi ⊢ ( ∃ 𝑣 ∈ 𝑈 ( ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ ∪ 𝑥 )
22 19 21 sylbir ⊢ ( ( ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ ∪ 𝑥 )
23 18 11 22 syl2anc ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ∪ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑝 ∈ 𝑦 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ ∪ 𝑥 )
24 eluni2 ⊢ ( 𝑝 ∈ ∪ 𝑥 ↔ ∃ 𝑦 ∈ 𝑥 𝑝 ∈ 𝑦 )
25 24 biimpi ⊢ ( 𝑝 ∈ ∪ 𝑥 → ∃ 𝑦 ∈ 𝑥 𝑝 ∈ 𝑦 )
26 25 adantl ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ∪ 𝑥 ) → ∃ 𝑦 ∈ 𝑥 𝑝 ∈ 𝑦 )
27 23 26 r19.29a ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ∪ 𝑥 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ ∪ 𝑥 )
28 27 ralrimiva ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) → ∀ 𝑝 ∈ ∪ 𝑥 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ ∪ 𝑥 )
29 elutop ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ↔ ( ∪ 𝑥 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ ∪ 𝑥 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ ∪ 𝑥 ) ) )
30 29 adantr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) → ( ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ↔ ( ∪ 𝑥 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ ∪ 𝑥 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ ∪ 𝑥 ) ) )
31 8 28 30 mpbir2and ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) → ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) )
32 31 ex ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑥 ⊆ ( unifTop ‘ 𝑈 ) → ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) )
33 32 alrimiv ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∀ 𝑥 ( 𝑥 ⊆ ( unifTop ‘ 𝑈 ) → ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) )
34 elutop ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑥 ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ) ) )
35 34 biimpa ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) → ( 𝑥 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑥 ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ) )
36 35 simpld ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) → 𝑥 ⊆ 𝑋 )
37 36 adantrr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) → 𝑥 ⊆ 𝑋 )
38 ssinss1 ⊢ ( 𝑥 ⊆ 𝑋 → ( 𝑥 ∩ 𝑦 ) ⊆ 𝑋 )
39 37 38 syl ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ 𝑋 )
40 simpl ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
41 simpr31 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → 𝑢 ∈ 𝑈 )
42 simpr32 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → 𝑣 ∈ 𝑈 )
43 ustincl ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ) → ( 𝑢 ∩ 𝑣 ) ∈ 𝑈 )
44 40 41 42 43 syl3anc ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( 𝑢 ∩ 𝑣 ) ∈ 𝑈 )
45 inss1 ⊢ ( 𝑢 ∩ 𝑣 ) ⊆ 𝑢
46 imass1 ⊢ ( ( 𝑢 ∩ 𝑣 ) ⊆ 𝑢 → ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑢 “ { 𝑝 } ) )
47 45 46 ax-mp ⊢ ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑢 “ { 𝑝 } )
48 simpr33 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) )
49 48 simpld ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 )
50 47 49 sstrid ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ 𝑥 )
51 inss2 ⊢ ( 𝑢 ∩ 𝑣 ) ⊆ 𝑣
52 imass1 ⊢ ( ( 𝑢 ∩ 𝑣 ) ⊆ 𝑣 → ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑣 “ { 𝑝 } ) )
53 51 52 ax-mp ⊢ ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑣 “ { 𝑝 } )
54 48 simprd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 )
55 53 54 sstrid ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ 𝑦 )
56 50 55 ssind ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) )
57 imaeq1 ⊢ ( 𝑤 = ( 𝑢 ∩ 𝑣 ) → ( 𝑤 “ { 𝑝 } ) = ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) )
58 57 sseq1d ⊢ ( 𝑤 = ( 𝑢 ∩ 𝑣 ) → ( ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ↔ ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ) )
59 58 rspcev ⊢ ( ( ( 𝑢 ∩ 𝑣 ) ∈ 𝑈 ∧ ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) )
60 44 56 59 syl2anc ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) )
61 60 3anassrs ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) )
62 61 3anassrs ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) )
63 simpll ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
64 simplrl ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑥 ∈ ( unifTop ‘ 𝑈 ) )
65 simpr ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) )
66 elin ⊢ ( 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ↔ ( 𝑝 ∈ 𝑥 ∧ 𝑝 ∈ 𝑦 ) )
67 65 66 sylib ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( 𝑝 ∈ 𝑥 ∧ 𝑝 ∈ 𝑦 ) )
68 67 simpld ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑝 ∈ 𝑥 )
69 35 simprd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) → ∀ 𝑝 ∈ 𝑥 ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 )
70 69 r19.21bi ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ 𝑥 ) → ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 )
71 63 64 68 70 syl21anc ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 )
72 simplrr ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑦 ∈ ( unifTop ‘ 𝑈 ) )
73 67 simprd ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑝 ∈ 𝑦 )
74 63 72 73 17 syl21anc ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 )
75 reeanv ⊢ ( ∃ 𝑢 ∈ 𝑈 ∃ 𝑣 ∈ 𝑈 ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ↔ ( ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) )
76 71 74 75 sylanbrc ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑢 ∈ 𝑈 ∃ 𝑣 ∈ 𝑈 ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) )
77 62 76 r19.29vva ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) )
78 77 ralrimiva ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) → ∀ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) )
79 elutop ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ( 𝑥 ∩ 𝑦 ) ∈ ( unifTop ‘ 𝑈 ) ↔ ( ( 𝑥 ∩ 𝑦 ) ⊆ 𝑋 ∧ ∀ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
80 79 adantr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) → ( ( 𝑥 ∩ 𝑦 ) ∈ ( unifTop ‘ 𝑈 ) ↔ ( ( 𝑥 ∩ 𝑦 ) ⊆ 𝑋 ∧ ∀ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
81 39 78 80 mpbir2and ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) → ( 𝑥 ∩ 𝑦 ) ∈ ( unifTop ‘ 𝑈 ) )
82 81 ralrimivva ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∀ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∀ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ( 𝑥 ∩ 𝑦 ) ∈ ( unifTop ‘ 𝑈 ) )
83 fvex ⊢ ( unifTop ‘ 𝑈 ) ∈ V
84 istopg ⊢ ( ( unifTop ‘ 𝑈 ) ∈ V → ( ( unifTop ‘ 𝑈 ) ∈ Top ↔ ( ∀ 𝑥 ( 𝑥 ⊆ ( unifTop ‘ 𝑈 ) → ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) ∧ ∀ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∀ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ( 𝑥 ∩ 𝑦 ) ∈ ( unifTop ‘ 𝑈 ) ) ) )
85 83 84 ax-mp ⊢ ( ( unifTop ‘ 𝑈 ) ∈ Top ↔ ( ∀ 𝑥 ( 𝑥 ⊆ ( unifTop ‘ 𝑈 ) → ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) ∧ ∀ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∀ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ( 𝑥 ∩ 𝑦 ) ∈ ( unifTop ‘ 𝑈 ) ) )
86 33 82 85 sylanbrc ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) ∈ Top )