Metamath Proof Explorer

Theorem ustfilxp

Description: A uniform structure on a nonempty base is a filter. Remark 3 of BourbakiTop1 p. II.2. (Contributed by Thierry Arnoux, 15-Nov-2017) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion ustfilxp ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) → 𝑈 ∈ ( Fil ‘ ( 𝑋 × 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 elfvex ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 ∈ V )
2 isust ⊢ ( 𝑋 ∈ V → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ↔ ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) ) )
3 1 2 syl ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ↔ ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) ) )
4 3 ibi ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) )
5 4 adantl ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) → ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) )
6 5 simp1d ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) → 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) )
7 5 simp2d ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) → ( 𝑋 × 𝑋 ) ∈ 𝑈 )
8 7 ne0d ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) → 𝑈 ≠ ∅ )
9 5 simp3d ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) → ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) )
10 9 r19.21bi ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) ∧ 𝑣 ∈ 𝑈 ) → ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) )
11 10 simp3d ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) ∧ 𝑣 ∈ 𝑈 ) → ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) )
12 11 simp1d ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) ∧ 𝑣 ∈ 𝑈 ) → ( I ↾ 𝑋 ) ⊆ 𝑣 )
13 opelidres ⊢ ( 𝑤 ∈ V → ( ⟨ 𝑤 , 𝑤 ⟩ ∈ ( I ↾ 𝑋 ) ↔ 𝑤 ∈ 𝑋 ) )
14 13 elv ⊢ ( ⟨ 𝑤 , 𝑤 ⟩ ∈ ( I ↾ 𝑋 ) ↔ 𝑤 ∈ 𝑋 )
15 14 biimpri ⊢ ( 𝑤 ∈ 𝑋 → ⟨ 𝑤 , 𝑤 ⟩ ∈ ( I ↾ 𝑋 ) )
16 15 rgen ⊢ ∀ 𝑤 ∈ 𝑋 ⟨ 𝑤 , 𝑤 ⟩ ∈ ( I ↾ 𝑋 )
17 r19.2z ⊢ ( ( 𝑋 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑋 ⟨ 𝑤 , 𝑤 ⟩ ∈ ( I ↾ 𝑋 ) ) → ∃ 𝑤 ∈ 𝑋 ⟨ 𝑤 , 𝑤 ⟩ ∈ ( I ↾ 𝑋 ) )
18 16 17 mpan2 ⊢ ( 𝑋 ≠ ∅ → ∃ 𝑤 ∈ 𝑋 ⟨ 𝑤 , 𝑤 ⟩ ∈ ( I ↾ 𝑋 ) )
19 18 ad2antrr ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) ∧ 𝑣 ∈ 𝑈 ) → ∃ 𝑤 ∈ 𝑋 ⟨ 𝑤 , 𝑤 ⟩ ∈ ( I ↾ 𝑋 ) )
20 ne0i ⊢ ( ⟨ 𝑤 , 𝑤 ⟩ ∈ ( I ↾ 𝑋 ) → ( I ↾ 𝑋 ) ≠ ∅ )
21 20 rexlimivw ⊢ ( ∃ 𝑤 ∈ 𝑋 ⟨ 𝑤 , 𝑤 ⟩ ∈ ( I ↾ 𝑋 ) → ( I ↾ 𝑋 ) ≠ ∅ )
22 19 21 syl ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) ∧ 𝑣 ∈ 𝑈 ) → ( I ↾ 𝑋 ) ≠ ∅ )
23 ssn0 ⊢ ( ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ( I ↾ 𝑋 ) ≠ ∅ ) → 𝑣 ≠ ∅ )
24 12 22 23 syl2anc ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) ∧ 𝑣 ∈ 𝑈 ) → 𝑣 ≠ ∅ )
25 24 nelrdva ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) → ¬ ∅ ∈ 𝑈 )
26 df-nel ⊢ ( ∅ ∉ 𝑈 ↔ ¬ ∅ ∈ 𝑈 )
27 25 26 sylibr ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) → ∅ ∉ 𝑈 )
28 10 simp2d ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) ∧ 𝑣 ∈ 𝑈 ) → ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 )
29 28 r19.21bi ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 ∈ 𝑈 ) → ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 )
30 vex ⊢ 𝑤 ∈ V
31 30 inex2 ⊢ ( 𝑣 ∩ 𝑤 ) ∈ V
32 31 pwid ⊢ ( 𝑣 ∩ 𝑤 ) ∈ 𝒫 ( 𝑣 ∩ 𝑤 )
33 32 a1i ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 ∈ 𝑈 ) → ( 𝑣 ∩ 𝑤 ) ∈ 𝒫 ( 𝑣 ∩ 𝑤 ) )
34 29 33 elind ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 ∈ 𝑈 ) → ( 𝑣 ∩ 𝑤 ) ∈ ( 𝑈 ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) )
35 34 ne0d ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 ∈ 𝑈 ) → ( 𝑈 ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ≠ ∅ )
36 35 ralrimiva ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) ∧ 𝑣 ∈ 𝑈 ) → ∀ 𝑤 ∈ 𝑈 ( 𝑈 ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ≠ ∅ )
37 36 ralrimiva ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) → ∀ 𝑣 ∈ 𝑈 ∀ 𝑤 ∈ 𝑈 ( 𝑈 ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ≠ ∅ )
38 8 27 37 3jca ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) → ( 𝑈 ≠ ∅ ∧ ∅ ∉ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ∀ 𝑤 ∈ 𝑈 ( 𝑈 ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ≠ ∅ ) )
39 1 1 xpexd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑋 × 𝑋 ) ∈ V )
40 isfbas ⊢ ( ( 𝑋 × 𝑋 ) ∈ V → ( 𝑈 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) ↔ ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑈 ≠ ∅ ∧ ∅ ∉ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ∀ 𝑤 ∈ 𝑈 ( 𝑈 ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ≠ ∅ ) ) ) )
41 39 40 syl ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑈 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) ↔ ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑈 ≠ ∅ ∧ ∅ ∉ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ∀ 𝑤 ∈ 𝑈 ( 𝑈 ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ≠ ∅ ) ) ) )
42 41 adantl ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) → ( 𝑈 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) ↔ ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑈 ≠ ∅ ∧ ∅ ∉ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ∀ 𝑤 ∈ 𝑈 ( 𝑈 ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ≠ ∅ ) ) ) )
43 6 38 42 mpbir2and ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) → 𝑈 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) )
44 n0 ⊢ ( ( 𝑈 ∩ 𝒫 𝑤 ) ≠ ∅ ↔ ∃ 𝑣 𝑣 ∈ ( 𝑈 ∩ 𝒫 𝑤 ) )
45 elin ⊢ ( 𝑣 ∈ ( 𝑈 ∩ 𝒫 𝑤 ) ↔ ( 𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝒫 𝑤 ) )
46 velpw ⊢ ( 𝑣 ∈ 𝒫 𝑤 ↔ 𝑣 ⊆ 𝑤 )
47 46 anbi2i ⊢ ( ( 𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝒫 𝑤 ) ↔ ( 𝑣 ∈ 𝑈 ∧ 𝑣 ⊆ 𝑤 ) )
48 45 47 bitri ⊢ ( 𝑣 ∈ ( 𝑈 ∩ 𝒫 𝑤 ) ↔ ( 𝑣 ∈ 𝑈 ∧ 𝑣 ⊆ 𝑤 ) )
49 48 exbii ⊢ ( ∃ 𝑣 𝑣 ∈ ( 𝑈 ∩ 𝒫 𝑤 ) ↔ ∃ 𝑣 ( 𝑣 ∈ 𝑈 ∧ 𝑣 ⊆ 𝑤 ) )
50 44 49 bitri ⊢ ( ( 𝑈 ∩ 𝒫 𝑤 ) ≠ ∅ ↔ ∃ 𝑣 ( 𝑣 ∈ 𝑈 ∧ 𝑣 ⊆ 𝑤 ) )
51 10 simp1d ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) ∧ 𝑣 ∈ 𝑈 ) → ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) )
52 51 r19.21bi ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ) → ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) )
53 52 an32s ⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) ∧ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ) ∧ 𝑣 ∈ 𝑈 ) → ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) )
54 53 expimpd ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) ∧ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ) → ( ( 𝑣 ∈ 𝑈 ∧ 𝑣 ⊆ 𝑤 ) → 𝑤 ∈ 𝑈 ) )
55 54 exlimdv ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) ∧ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ) → ( ∃ 𝑣 ( 𝑣 ∈ 𝑈 ∧ 𝑣 ⊆ 𝑤 ) → 𝑤 ∈ 𝑈 ) )
56 50 55 syl5bi ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) ∧ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ) → ( ( 𝑈 ∩ 𝒫 𝑤 ) ≠ ∅ → 𝑤 ∈ 𝑈 ) )
57 56 ralrimiva ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) → ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( ( 𝑈 ∩ 𝒫 𝑤 ) ≠ ∅ → 𝑤 ∈ 𝑈 ) )
58 isfil ⊢ ( 𝑈 ∈ ( Fil ‘ ( 𝑋 × 𝑋 ) ) ↔ ( 𝑈 ∈ ( fBas ‘ ( 𝑋 × 𝑋 ) ) ∧ ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( ( 𝑈 ∩ 𝒫 𝑤 ) ≠ ∅ → 𝑤 ∈ 𝑈 ) ) )
59 43 57 58 sylanbrc ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) → 𝑈 ∈ ( Fil ‘ ( 𝑋 × 𝑋 ) ) )