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 bilani ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ∪ 𝑥 ) → ∃ 𝑦 ∈ 𝑥 𝑝 ∈ 𝑦 )
26 23 25 r19.29a ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ∪ 𝑥 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ ∪ 𝑥 )
27 26 ralrimiva ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) → ∀ 𝑝 ∈ ∪ 𝑥 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ ∪ 𝑥 )
28 elutop ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ↔ ( ∪ 𝑥 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ ∪ 𝑥 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ ∪ 𝑥 ) ) )
29 28 adantr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) → ( ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ↔ ( ∪ 𝑥 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ ∪ 𝑥 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ ∪ 𝑥 ) ) )
30 8 27 29 mpbir2and ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ⊆ ( unifTop ‘ 𝑈 ) ) → ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) )
31 30 ex ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑥 ⊆ ( unifTop ‘ 𝑈 ) → ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) )
32 31 alrimiv ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∀ 𝑥 ( 𝑥 ⊆ ( unifTop ‘ 𝑈 ) → ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) )
33 elutop ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑥 ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ) ) )
34 33 biimpa ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) → ( 𝑥 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝑥 ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ) )
35 34 simpld ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) → 𝑥 ⊆ 𝑋 )
36 35 adantrr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) → 𝑥 ⊆ 𝑋 )
37 ssinss1 ⊢ ( 𝑥 ⊆ 𝑋 → ( 𝑥 ∩ 𝑦 ) ⊆ 𝑋 )
38 36 37 syl ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ 𝑋 )
39 simpl ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
40 simpr31 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → 𝑢 ∈ 𝑈 )
41 simpr32 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → 𝑣 ∈ 𝑈 )
42 ustincl ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ) → ( 𝑢 ∩ 𝑣 ) ∈ 𝑈 )
43 39 40 41 42 syl3anc ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( 𝑢 ∩ 𝑣 ) ∈ 𝑈 )
44 inss1 ⊢ ( 𝑢 ∩ 𝑣 ) ⊆ 𝑢
45 imass1 ⊢ ( ( 𝑢 ∩ 𝑣 ) ⊆ 𝑢 → ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑢 “ { 𝑝 } ) )
46 44 45 ax-mp ⊢ ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑢 “ { 𝑝 } )
47 simpr33 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) )
48 47 simpld ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 )
49 46 48 sstrid ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ 𝑥 )
50 inss2 ⊢ ( 𝑢 ∩ 𝑣 ) ⊆ 𝑣
51 imass1 ⊢ ( ( 𝑢 ∩ 𝑣 ) ⊆ 𝑣 → ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑣 “ { 𝑝 } ) )
52 50 51 ax-mp ⊢ ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑣 “ { 𝑝 } )
53 47 simprd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 )
54 52 53 sstrid ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ 𝑦 )
55 49 54 ssind ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) )
56 imaeq1 ⊢ ( 𝑤 = ( 𝑢 ∩ 𝑣 ) → ( 𝑤 “ { 𝑝 } ) = ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) )
57 56 sseq1d ⊢ ( 𝑤 = ( 𝑢 ∩ 𝑣 ) → ( ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ↔ ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ) )
58 57 rspcev ⊢ ( ( ( 𝑢 ∩ 𝑣 ) ∈ 𝑈 ∧ ( ( 𝑢 ∩ 𝑣 ) “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) )
59 43 55 58 syl2anc ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) )
60 59 3anassrs ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑢 ∈ 𝑈 ∧ 𝑣 ∈ 𝑈 ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) )
61 60 3anassrs ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ 𝑢 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) )
62 simpll ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
63 simplrl ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑥 ∈ ( unifTop ‘ 𝑈 ) )
64 elin ⊢ ( 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ↔ ( 𝑝 ∈ 𝑥 ∧ 𝑝 ∈ 𝑦 ) )
65 64 bilani ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( 𝑝 ∈ 𝑥 ∧ 𝑝 ∈ 𝑦 ) )
66 65 simpld ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑝 ∈ 𝑥 )
67 34 simprd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) → ∀ 𝑝 ∈ 𝑥 ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 )
68 67 r19.21bi ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) ∧ 𝑝 ∈ 𝑥 ) → ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 )
69 62 63 66 68 syl21anc ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 )
70 simplrr ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑦 ∈ ( unifTop ‘ 𝑈 ) )
71 65 simprd ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑝 ∈ 𝑦 )
72 62 70 71 17 syl21anc ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 )
73 reeanv ⊢ ( ∃ 𝑢 ∈ 𝑈 ∃ 𝑣 ∈ 𝑈 ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) ↔ ( ∃ 𝑢 ∈ 𝑈 ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) )
74 69 72 73 sylanbrc ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑢 ∈ 𝑈 ∃ 𝑣 ∈ 𝑈 ( ( 𝑢 “ { 𝑝 } ) ⊆ 𝑥 ∧ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑦 ) )
75 61 74 r19.29vva ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) ∧ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) )
76 75 ralrimiva ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) → ∀ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) )
77 elutop ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ( 𝑥 ∩ 𝑦 ) ∈ ( unifTop ‘ 𝑈 ) ↔ ( ( 𝑥 ∩ 𝑦 ) ⊆ 𝑋 ∧ ∀ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
78 77 adantr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) → ( ( 𝑥 ∩ 𝑦 ) ∈ ( unifTop ‘ 𝑈 ) ↔ ( ( 𝑥 ∩ 𝑦 ) ⊆ 𝑋 ∧ ∀ 𝑝 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝑈 ( 𝑤 “ { 𝑝 } ) ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
79 38 76 78 mpbir2and ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∧ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ) ) → ( 𝑥 ∩ 𝑦 ) ∈ ( unifTop ‘ 𝑈 ) )
80 79 ralrimivva ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∀ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∀ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ( 𝑥 ∩ 𝑦 ) ∈ ( unifTop ‘ 𝑈 ) )
81 fvex ⊢ ( unifTop ‘ 𝑈 ) ∈ V
82 istopg ⊢ ( ( unifTop ‘ 𝑈 ) ∈ V → ( ( unifTop ‘ 𝑈 ) ∈ Top ↔ ( ∀ 𝑥 ( 𝑥 ⊆ ( unifTop ‘ 𝑈 ) → ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) ∧ ∀ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∀ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ( 𝑥 ∩ 𝑦 ) ∈ ( unifTop ‘ 𝑈 ) ) ) )
83 81 82 ax-mp ⊢ ( ( unifTop ‘ 𝑈 ) ∈ Top ↔ ( ∀ 𝑥 ( 𝑥 ⊆ ( unifTop ‘ 𝑈 ) → ∪ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ) ∧ ∀ 𝑥 ∈ ( unifTop ‘ 𝑈 ) ∀ 𝑦 ∈ ( unifTop ‘ 𝑈 ) ( 𝑥 ∩ 𝑦 ) ∈ ( unifTop ‘ 𝑈 ) ) )
84 32 80 83 sylanbrc ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) ∈ Top )