MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ustfilxp Structured version   Visualization version   GIF version

Theorem ustfilxp 24237
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.)
Assertion
Ref Expression
ustfilxp ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → 𝑈 ∈ (Fil‘(𝑋 × 𝑋)))

Proof of Theorem ustfilxp
Dummy variables 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfvex 6945 . . . . . . 7 (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ∈ V)
2 isust 24228 . . . . . . 7 (𝑋 ∈ V → (𝑈 ∈ (UnifOn‘𝑋) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣𝑤𝑤𝑈) ∧ ∀𝑤𝑈 (𝑣𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣𝑣𝑈 ∧ ∃𝑤𝑈 (𝑤𝑤) ⊆ 𝑣)))))
31, 2syl 17 . . . . . 6 (𝑈 ∈ (UnifOn‘𝑋) → (𝑈 ∈ (UnifOn‘𝑋) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣𝑤𝑤𝑈) ∧ ∀𝑤𝑈 (𝑣𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣𝑣𝑈 ∧ ∃𝑤𝑈 (𝑤𝑤) ⊆ 𝑣)))))
43ibi 267 . . . . 5 (𝑈 ∈ (UnifOn‘𝑋) → (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣𝑤𝑤𝑈) ∧ ∀𝑤𝑈 (𝑣𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣𝑣𝑈 ∧ ∃𝑤𝑈 (𝑤𝑤) ⊆ 𝑣))))
54adantl 481 . . . 4 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣𝑤𝑤𝑈) ∧ ∀𝑤𝑈 (𝑣𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣𝑣𝑈 ∧ ∃𝑤𝑈 (𝑤𝑤) ⊆ 𝑣))))
65simp1d 1141 . . 3 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → 𝑈 ⊆ 𝒫 (𝑋 × 𝑋))
75simp2d 1142 . . . . 5 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → (𝑋 × 𝑋) ∈ 𝑈)
87ne0d 4348 . . . 4 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → 𝑈 ≠ ∅)
95simp3d 1143 . . . . . . . . . 10 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → ∀𝑣𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣𝑤𝑤𝑈) ∧ ∀𝑤𝑈 (𝑣𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣𝑣𝑈 ∧ ∃𝑤𝑈 (𝑤𝑤) ⊆ 𝑣)))
109r19.21bi 3249 . . . . . . . . 9 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) → (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣𝑤𝑤𝑈) ∧ ∀𝑤𝑈 (𝑣𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣𝑣𝑈 ∧ ∃𝑤𝑈 (𝑤𝑤) ⊆ 𝑣)))
1110simp3d 1143 . . . . . . . 8 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) → (( I ↾ 𝑋) ⊆ 𝑣𝑣𝑈 ∧ ∃𝑤𝑈 (𝑤𝑤) ⊆ 𝑣))
1211simp1d 1141 . . . . . . 7 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) → ( I ↾ 𝑋) ⊆ 𝑣)
13 opelidres 6012 . . . . . . . . . . . . 13 (𝑤 ∈ V → (⟨𝑤, 𝑤⟩ ∈ ( I ↾ 𝑋) ↔ 𝑤𝑋))
1413elv 3483 . . . . . . . . . . . 12 (⟨𝑤, 𝑤⟩ ∈ ( I ↾ 𝑋) ↔ 𝑤𝑋)
1514biimpri 228 . . . . . . . . . . 11 (𝑤𝑋 → ⟨𝑤, 𝑤⟩ ∈ ( I ↾ 𝑋))
1615rgen 3061 . . . . . . . . . 10 𝑤𝑋𝑤, 𝑤⟩ ∈ ( I ↾ 𝑋)
17 r19.2z 4501 . . . . . . . . . 10 ((𝑋 ≠ ∅ ∧ ∀𝑤𝑋𝑤, 𝑤⟩ ∈ ( I ↾ 𝑋)) → ∃𝑤𝑋𝑤, 𝑤⟩ ∈ ( I ↾ 𝑋))
1816, 17mpan2 691 . . . . . . . . 9 (𝑋 ≠ ∅ → ∃𝑤𝑋𝑤, 𝑤⟩ ∈ ( I ↾ 𝑋))
1918ad2antrr 726 . . . . . . . 8 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) → ∃𝑤𝑋𝑤, 𝑤⟩ ∈ ( I ↾ 𝑋))
20 ne0i 4347 . . . . . . . . 9 (⟨𝑤, 𝑤⟩ ∈ ( I ↾ 𝑋) → ( I ↾ 𝑋) ≠ ∅)
2120rexlimivw 3149 . . . . . . . 8 (∃𝑤𝑋𝑤, 𝑤⟩ ∈ ( I ↾ 𝑋) → ( I ↾ 𝑋) ≠ ∅)
2219, 21syl 17 . . . . . . 7 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) → ( I ↾ 𝑋) ≠ ∅)
23 ssn0 4410 . . . . . . 7 ((( I ↾ 𝑋) ⊆ 𝑣 ∧ ( I ↾ 𝑋) ≠ ∅) → 𝑣 ≠ ∅)
2412, 22, 23syl2anc 584 . . . . . 6 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) → 𝑣 ≠ ∅)
2524nelrdva 3714 . . . . 5 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → ¬ ∅ ∈ 𝑈)
26 df-nel 3045 . . . . 5 (∅ ∉ 𝑈 ↔ ¬ ∅ ∈ 𝑈)
2725, 26sylibr 234 . . . 4 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → ∅ ∉ 𝑈)
2810simp2d 1142 . . . . . . . . 9 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) → ∀𝑤𝑈 (𝑣𝑤) ∈ 𝑈)
2928r19.21bi 3249 . . . . . . . 8 ((((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) ∧ 𝑤𝑈) → (𝑣𝑤) ∈ 𝑈)
30 vex 3482 . . . . . . . . . . 11 𝑤 ∈ V
3130inex2 5324 . . . . . . . . . 10 (𝑣𝑤) ∈ V
3231pwid 4627 . . . . . . . . 9 (𝑣𝑤) ∈ 𝒫 (𝑣𝑤)
3332a1i 11 . . . . . . . 8 ((((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) ∧ 𝑤𝑈) → (𝑣𝑤) ∈ 𝒫 (𝑣𝑤))
3429, 33elind 4210 . . . . . . 7 ((((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) ∧ 𝑤𝑈) → (𝑣𝑤) ∈ (𝑈 ∩ 𝒫 (𝑣𝑤)))
3534ne0d 4348 . . . . . 6 ((((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) ∧ 𝑤𝑈) → (𝑈 ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
3635ralrimiva 3144 . . . . 5 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) → ∀𝑤𝑈 (𝑈 ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
3736ralrimiva 3144 . . . 4 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → ∀𝑣𝑈𝑤𝑈 (𝑈 ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
388, 27, 373jca 1127 . . 3 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → (𝑈 ≠ ∅ ∧ ∅ ∉ 𝑈 ∧ ∀𝑣𝑈𝑤𝑈 (𝑈 ∩ 𝒫 (𝑣𝑤)) ≠ ∅))
391, 1xpexd 7770 . . . . 5 (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) ∈ V)
40 isfbas 23853 . . . . 5 ((𝑋 × 𝑋) ∈ V → (𝑈 ∈ (fBas‘(𝑋 × 𝑋)) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑈 ≠ ∅ ∧ ∅ ∉ 𝑈 ∧ ∀𝑣𝑈𝑤𝑈 (𝑈 ∩ 𝒫 (𝑣𝑤)) ≠ ∅))))
4139, 40syl 17 . . . 4 (𝑈 ∈ (UnifOn‘𝑋) → (𝑈 ∈ (fBas‘(𝑋 × 𝑋)) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑈 ≠ ∅ ∧ ∅ ∉ 𝑈 ∧ ∀𝑣𝑈𝑤𝑈 (𝑈 ∩ 𝒫 (𝑣𝑤)) ≠ ∅))))
4241adantl 481 . . 3 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → (𝑈 ∈ (fBas‘(𝑋 × 𝑋)) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑈 ≠ ∅ ∧ ∅ ∉ 𝑈 ∧ ∀𝑣𝑈𝑤𝑈 (𝑈 ∩ 𝒫 (𝑣𝑤)) ≠ ∅))))
436, 38, 42mpbir2and 713 . 2 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → 𝑈 ∈ (fBas‘(𝑋 × 𝑋)))
44 n0 4359 . . . . 5 ((𝑈 ∩ 𝒫 𝑤) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ (𝑈 ∩ 𝒫 𝑤))
45 elin 3979 . . . . . . 7 (𝑣 ∈ (𝑈 ∩ 𝒫 𝑤) ↔ (𝑣𝑈𝑣 ∈ 𝒫 𝑤))
46 velpw 4610 . . . . . . . 8 (𝑣 ∈ 𝒫 𝑤𝑣𝑤)
4746anbi2i 623 . . . . . . 7 ((𝑣𝑈𝑣 ∈ 𝒫 𝑤) ↔ (𝑣𝑈𝑣𝑤))
4845, 47bitri 275 . . . . . 6 (𝑣 ∈ (𝑈 ∩ 𝒫 𝑤) ↔ (𝑣𝑈𝑣𝑤))
4948exbii 1845 . . . . 5 (∃𝑣 𝑣 ∈ (𝑈 ∩ 𝒫 𝑤) ↔ ∃𝑣(𝑣𝑈𝑣𝑤))
5044, 49bitri 275 . . . 4 ((𝑈 ∩ 𝒫 𝑤) ≠ ∅ ↔ ∃𝑣(𝑣𝑈𝑣𝑤))
5110simp1d 1141 . . . . . . . 8 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) → ∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣𝑤𝑤𝑈))
5251r19.21bi 3249 . . . . . . 7 ((((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) ∧ 𝑤 ∈ 𝒫 (𝑋 × 𝑋)) → (𝑣𝑤𝑤𝑈))
5352an32s 652 . . . . . 6 ((((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑤 ∈ 𝒫 (𝑋 × 𝑋)) ∧ 𝑣𝑈) → (𝑣𝑤𝑤𝑈))
5453expimpd 453 . . . . 5 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑤 ∈ 𝒫 (𝑋 × 𝑋)) → ((𝑣𝑈𝑣𝑤) → 𝑤𝑈))
5554exlimdv 1931 . . . 4 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑤 ∈ 𝒫 (𝑋 × 𝑋)) → (∃𝑣(𝑣𝑈𝑣𝑤) → 𝑤𝑈))
5650, 55biimtrid 242 . . 3 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑤 ∈ 𝒫 (𝑋 × 𝑋)) → ((𝑈 ∩ 𝒫 𝑤) ≠ ∅ → 𝑤𝑈))
5756ralrimiva 3144 . 2 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → ∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)((𝑈 ∩ 𝒫 𝑤) ≠ ∅ → 𝑤𝑈))
58 isfil 23871 . 2 (𝑈 ∈ (Fil‘(𝑋 × 𝑋)) ↔ (𝑈 ∈ (fBas‘(𝑋 × 𝑋)) ∧ ∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)((𝑈 ∩ 𝒫 𝑤) ≠ ∅ → 𝑤𝑈)))
5943, 57, 58sylanbrc 583 1 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → 𝑈 ∈ (Fil‘(𝑋 × 𝑋)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086  wex 1776  wcel 2106  wne 2938  wnel 3044  wral 3059  wrex 3068  Vcvv 3478  cin 3962  wss 3963  c0 4339  𝒫 cpw 4605  cop 4637   I cid 5582   × cxp 5687  ccnv 5688  cres 5691  ccom 5693  cfv 6563  fBascfbas 21370  Filcfil 23869  UnifOncust 24224
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fv 6571  df-fbas 21379  df-fil 23870  df-ust 24225
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator