Metamath Proof Explorer

Theorem metust

Description: The uniform structure generated by a metric D . (Contributed by Thierry Arnoux, 26-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Hypothesis metust.1 ⊢ 𝐹 = ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
Assertion metust ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( UnifOn ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 metust.1 ⊢ 𝐹 = ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
2 1 metustfbas ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) )
3 fgcl ⊢ ( 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) → ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( Fil ‘ ( 𝑋 × 𝑋 ) ) )
4 filsspw ⊢ ( ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( Fil ‘ ( 𝑋 × 𝑋 ) ) → ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ⊆ 𝒫 ( 𝑋 × 𝑋 ) )
5 2 3 4 3syl ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ⊆ 𝒫 ( 𝑋 × 𝑋 ) )
6 filtop ⊢ ( ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( Fil ‘ ( 𝑋 × 𝑋 ) ) → ( 𝑋 × 𝑋 ) ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
7 2 3 6 3syl ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑋 × 𝑋 ) ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
8 2 3 syl ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( Fil ‘ ( 𝑋 × 𝑋 ) ) )
9 8 ad3antrrr ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ) ∧ 𝑣 ⊆ 𝑤 ) → ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( Fil ‘ ( 𝑋 × 𝑋 ) ) )
10 simpllr ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ) ∧ 𝑣 ⊆ 𝑤 ) → 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
11 simplr ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ) ∧ 𝑣 ⊆ 𝑤 ) → 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) )
12 11 elpwid ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ) ∧ 𝑣 ⊆ 𝑤 ) → 𝑤 ⊆ ( 𝑋 × 𝑋 ) )
13 simpr ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ) ∧ 𝑣 ⊆ 𝑤 ) → 𝑣 ⊆ 𝑤 )
14 filss ⊢ ( ( ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( Fil ‘ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∧ 𝑤 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑣 ⊆ 𝑤 ) ) → 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
15 9 10 12 13 14 syl13anc ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ) ∧ 𝑣 ⊆ 𝑤 ) → 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
16 15 ex ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ) → ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) )
17 16 ralrimiva ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) )
18 8 ad2antrr ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( Fil ‘ ( 𝑋 × 𝑋 ) ) )
19 simplr ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
20 simpr ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
21 filin ⊢ ( ( ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( Fil ‘ ( 𝑋 × 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∧ 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ( 𝑣 ∩ 𝑤 ) ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
22 18 19 20 21 syl3anc ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ( 𝑣 ∩ 𝑤 ) ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
23 22 ralrimiva ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ∀ 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ( 𝑣 ∩ 𝑤 ) ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
24 1 metustid ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑢 ∈ 𝐹 ) → ( I ↾ 𝑋 ) ⊆ 𝑢 )
25 24 ad5ant24 ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑢 ∈ 𝐹 ) ∧ 𝑢 ⊆ 𝑣 ) → ( I ↾ 𝑋 ) ⊆ 𝑢 )
26 simpr ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑢 ∈ 𝐹 ) ∧ 𝑢 ⊆ 𝑣 ) → 𝑢 ⊆ 𝑣 )
27 25 26 sstrd ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑢 ∈ 𝐹 ) ∧ 𝑢 ⊆ 𝑣 ) → ( I ↾ 𝑋 ) ⊆ 𝑣 )
28 elfg ⊢ ( 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) → ( 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ↔ ( 𝑣 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑢 ∈ 𝐹 𝑢 ⊆ 𝑣 ) ) )
29 28 biimpa ⊢ ( ( 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ( 𝑣 ⊆ ( 𝑋 × 𝑋 ) ∧ ∃ 𝑢 ∈ 𝐹 𝑢 ⊆ 𝑣 ) )
30 29 simprd ⊢ ( ( 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ∃ 𝑢 ∈ 𝐹 𝑢 ⊆ 𝑣 )
31 2 30 sylan ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ∃ 𝑢 ∈ 𝐹 𝑢 ⊆ 𝑣 )
32 27 31 r19.29a ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ( I ↾ 𝑋 ) ⊆ 𝑣 )
33 8 ad3antrrr ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑢 ∈ 𝐹 ) ∧ 𝑢 ⊆ 𝑣 ) → ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( Fil ‘ ( 𝑋 × 𝑋 ) ) )
34 2 adantr ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) )
35 ssfg ⊢ ( 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) → 𝐹 ⊆ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
36 34 35 syl ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → 𝐹 ⊆ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
37 36 ad2antrr ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑢 ∈ 𝐹 ) ∧ 𝑢 ⊆ 𝑣 ) → 𝐹 ⊆ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
38 simplr ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑢 ∈ 𝐹 ) ∧ 𝑢 ⊆ 𝑣 ) → 𝑢 ∈ 𝐹 )
39 37 38 sseldd ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑢 ∈ 𝐹 ) ∧ 𝑢 ⊆ 𝑣 ) → 𝑢 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
40 29 simpld ⊢ ( ( 𝐹 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → 𝑣 ⊆ ( 𝑋 × 𝑋 ) )
41 2 40 sylan ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → 𝑣 ⊆ ( 𝑋 × 𝑋 ) )
42 41 ad2antrr ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑢 ∈ 𝐹 ) ∧ 𝑢 ⊆ 𝑣 ) → 𝑣 ⊆ ( 𝑋 × 𝑋 ) )
43 cnvss ⊢ ( 𝑣 ⊆ ( 𝑋 × 𝑋 ) → ◡ 𝑣 ⊆ ◡ ( 𝑋 × 𝑋 ) )
44 cnvxp ⊢ ◡ ( 𝑋 × 𝑋 ) = ( 𝑋 × 𝑋 )
45 43 44 sseqtrdi ⊢ ( 𝑣 ⊆ ( 𝑋 × 𝑋 ) → ◡ 𝑣 ⊆ ( 𝑋 × 𝑋 ) )
46 42 45 syl ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑢 ∈ 𝐹 ) ∧ 𝑢 ⊆ 𝑣 ) → ◡ 𝑣 ⊆ ( 𝑋 × 𝑋 ) )
47 1 metustsym ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑢 ∈ 𝐹 ) → ◡ 𝑢 = 𝑢 )
48 47 ad5ant24 ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑢 ∈ 𝐹 ) ∧ 𝑢 ⊆ 𝑣 ) → ◡ 𝑢 = 𝑢 )
49 cnvss ⊢ ( 𝑢 ⊆ 𝑣 → ◡ 𝑢 ⊆ ◡ 𝑣 )
50 49 adantl ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑢 ∈ 𝐹 ) ∧ 𝑢 ⊆ 𝑣 ) → ◡ 𝑢 ⊆ ◡ 𝑣 )
51 48 50 eqsstrrd ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑢 ∈ 𝐹 ) ∧ 𝑢 ⊆ 𝑣 ) → 𝑢 ⊆ ◡ 𝑣 )
52 filss ⊢ ( ( ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( Fil ‘ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑢 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∧ ◡ 𝑣 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑢 ⊆ ◡ 𝑣 ) ) → ◡ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
53 33 39 46 51 52 syl13anc ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑢 ∈ 𝐹 ) ∧ 𝑢 ⊆ 𝑣 ) → ◡ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
54 53 31 r19.29a ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ◡ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) )
55 1 metustexhalf ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑢 ∈ 𝐹 ) → ∃ 𝑤 ∈ 𝐹 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑢 )
56 55 ad4ant13 ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑢 ∈ 𝐹 ) ∧ 𝑢 ⊆ 𝑣 ) → ∃ 𝑤 ∈ 𝐹 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑢 )
57 r19.41v ⊢ ( ∃ 𝑤 ∈ 𝐹 ( ( 𝑤 ∘ 𝑤 ) ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑣 ) ↔ ( ∃ 𝑤 ∈ 𝐹 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑣 ) )
58 sstr ⊢ ( ( ( 𝑤 ∘ 𝑤 ) ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑣 ) → ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 )
59 58 reximi ⊢ ( ∃ 𝑤 ∈ 𝐹 ( ( 𝑤 ∘ 𝑤 ) ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑣 ) → ∃ 𝑤 ∈ 𝐹 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 )
60 57 59 sylbir ⊢ ( ( ∃ 𝑤 ∈ 𝐹 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑣 ) → ∃ 𝑤 ∈ 𝐹 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 )
61 56 60 sylancom ⊢ ( ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ 𝑢 ∈ 𝐹 ) ∧ 𝑢 ⊆ 𝑣 ) → ∃ 𝑤 ∈ 𝐹 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 )
62 61 31 r19.29a ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ∃ 𝑤 ∈ 𝐹 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 )
63 ssrexv ⊢ ( 𝐹 ⊆ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) → ( ∃ 𝑤 ∈ 𝐹 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 → ∃ 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) )
64 36 62 63 sylc ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ∃ 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 )
65 32 54 64 3jca ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∧ ∃ 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) )
66 17 23 65 3jca ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) ∧ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) → ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ ∀ 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ( 𝑣 ∩ 𝑤 ) ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∧ ∃ 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) )
67 66 ralrimiva ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ∀ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ ∀ 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ( 𝑣 ∩ 𝑤 ) ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∧ ∃ 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) )
68 elfvex ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ V )
69 68 adantl ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → 𝑋 ∈ V )
70 isust ⊢ ( 𝑋 ∈ V → ( ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( UnifOn ‘ 𝑋 ) ↔ ( ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∧ ∀ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ ∀ 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ( 𝑣 ∩ 𝑤 ) ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∧ ∃ 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) ) )
71 69 70 syl ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( UnifOn ‘ 𝑋 ) ↔ ( ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∧ ∀ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ) ∧ ∀ 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ( 𝑣 ∩ 𝑤 ) ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∧ ∃ 𝑤 ∈ ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) ) )
72 5 7 67 71 mpbir3and ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( ( 𝑋 × 𝑋 ) filGen 𝐹 ) ∈ ( UnifOn ‘ 𝑋 ) )