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

Theorem ustfilxp 24222
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 6943 . . . . . . 7 (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ∈ V)
2 isust 24213 . . . . . . 7 (𝑋 ∈ V → (𝑈 ∈ (UnifOn‘𝑋) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣𝑤𝑤𝑈) ∧ ∀𝑤𝑈 (𝑣𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣𝑣𝑈 ∧ ∃𝑤𝑈 (𝑤𝑤) ⊆ 𝑣)))))
31, 2syl 17 . . . . . 6 (𝑈 ∈ (UnifOn‘𝑋) → (𝑈 ∈ (UnifOn‘𝑋) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣𝑤𝑤𝑈) ∧ ∀𝑤𝑈 (𝑣𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣𝑣𝑈 ∧ ∃𝑤𝑈 (𝑤𝑤) ⊆ 𝑣)))))
43ibi 267 . . . . 5 (𝑈 ∈ (UnifOn‘𝑋) → (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣𝑤𝑤𝑈) ∧ ∀𝑤𝑈 (𝑣𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣𝑣𝑈 ∧ ∃𝑤𝑈 (𝑤𝑤) ⊆ 𝑣))))
54adantl 481 . . . 4 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣𝑤𝑤𝑈) ∧ ∀𝑤𝑈 (𝑣𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣𝑣𝑈 ∧ ∃𝑤𝑈 (𝑤𝑤) ⊆ 𝑣))))
65simp1d 1142 . . 3 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → 𝑈 ⊆ 𝒫 (𝑋 × 𝑋))
75simp2d 1143 . . . . 5 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → (𝑋 × 𝑋) ∈ 𝑈)
87ne0d 4341 . . . 4 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → 𝑈 ≠ ∅)
95simp3d 1144 . . . . . . . . . 10 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → ∀𝑣𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣𝑤𝑤𝑈) ∧ ∀𝑤𝑈 (𝑣𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣𝑣𝑈 ∧ ∃𝑤𝑈 (𝑤𝑤) ⊆ 𝑣)))
109r19.21bi 3250 . . . . . . . . 9 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) → (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣𝑤𝑤𝑈) ∧ ∀𝑤𝑈 (𝑣𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣𝑣𝑈 ∧ ∃𝑤𝑈 (𝑤𝑤) ⊆ 𝑣)))
1110simp3d 1144 . . . . . . . 8 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) → (( I ↾ 𝑋) ⊆ 𝑣𝑣𝑈 ∧ ∃𝑤𝑈 (𝑤𝑤) ⊆ 𝑣))
1211simp1d 1142 . . . . . . 7 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) → ( I ↾ 𝑋) ⊆ 𝑣)
13 opelidres 6008 . . . . . . . . . . . . 13 (𝑤 ∈ V → (⟨𝑤, 𝑤⟩ ∈ ( I ↾ 𝑋) ↔ 𝑤𝑋))
1413elv 3484 . . . . . . . . . . . 12 (⟨𝑤, 𝑤⟩ ∈ ( I ↾ 𝑋) ↔ 𝑤𝑋)
1514biimpri 228 . . . . . . . . . . 11 (𝑤𝑋 → ⟨𝑤, 𝑤⟩ ∈ ( I ↾ 𝑋))
1615rgen 3062 . . . . . . . . . 10 𝑤𝑋𝑤, 𝑤⟩ ∈ ( I ↾ 𝑋)
17 r19.2z 4494 . . . . . . . . . 10 ((𝑋 ≠ ∅ ∧ ∀𝑤𝑋𝑤, 𝑤⟩ ∈ ( I ↾ 𝑋)) → ∃𝑤𝑋𝑤, 𝑤⟩ ∈ ( I ↾ 𝑋))
1816, 17mpan2 691 . . . . . . . . 9 (𝑋 ≠ ∅ → ∃𝑤𝑋𝑤, 𝑤⟩ ∈ ( I ↾ 𝑋))
1918ad2antrr 726 . . . . . . . 8 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) → ∃𝑤𝑋𝑤, 𝑤⟩ ∈ ( I ↾ 𝑋))
20 ne0i 4340 . . . . . . . . 9 (⟨𝑤, 𝑤⟩ ∈ ( I ↾ 𝑋) → ( I ↾ 𝑋) ≠ ∅)
2120rexlimivw 3150 . . . . . . . 8 (∃𝑤𝑋𝑤, 𝑤⟩ ∈ ( I ↾ 𝑋) → ( I ↾ 𝑋) ≠ ∅)
2219, 21syl 17 . . . . . . 7 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) → ( I ↾ 𝑋) ≠ ∅)
23 ssn0 4403 . . . . . . 7 ((( I ↾ 𝑋) ⊆ 𝑣 ∧ ( I ↾ 𝑋) ≠ ∅) → 𝑣 ≠ ∅)
2412, 22, 23syl2anc 584 . . . . . 6 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) → 𝑣 ≠ ∅)
2524nelrdva 3710 . . . . 5 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → ¬ ∅ ∈ 𝑈)
26 df-nel 3046 . . . . 5 (∅ ∉ 𝑈 ↔ ¬ ∅ ∈ 𝑈)
2725, 26sylibr 234 . . . 4 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → ∅ ∉ 𝑈)
2810simp2d 1143 . . . . . . . . 9 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) → ∀𝑤𝑈 (𝑣𝑤) ∈ 𝑈)
2928r19.21bi 3250 . . . . . . . 8 ((((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) ∧ 𝑤𝑈) → (𝑣𝑤) ∈ 𝑈)
30 vex 3483 . . . . . . . . . . 11 𝑤 ∈ V
3130inex2 5317 . . . . . . . . . 10 (𝑣𝑤) ∈ V
3231pwid 4621 . . . . . . . . 9 (𝑣𝑤) ∈ 𝒫 (𝑣𝑤)
3332a1i 11 . . . . . . . 8 ((((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) ∧ 𝑤𝑈) → (𝑣𝑤) ∈ 𝒫 (𝑣𝑤))
3429, 33elind 4199 . . . . . . 7 ((((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) ∧ 𝑤𝑈) → (𝑣𝑤) ∈ (𝑈 ∩ 𝒫 (𝑣𝑤)))
3534ne0d 4341 . . . . . 6 ((((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) ∧ 𝑤𝑈) → (𝑈 ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
3635ralrimiva 3145 . . . . 5 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) → ∀𝑤𝑈 (𝑈 ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
3736ralrimiva 3145 . . . 4 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → ∀𝑣𝑈𝑤𝑈 (𝑈 ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
388, 27, 373jca 1128 . . 3 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → (𝑈 ≠ ∅ ∧ ∅ ∉ 𝑈 ∧ ∀𝑣𝑈𝑤𝑈 (𝑈 ∩ 𝒫 (𝑣𝑤)) ≠ ∅))
391, 1xpexd 7772 . . . . 5 (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) ∈ V)
40 isfbas 23838 . . . . 5 ((𝑋 × 𝑋) ∈ V → (𝑈 ∈ (fBas‘(𝑋 × 𝑋)) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑈 ≠ ∅ ∧ ∅ ∉ 𝑈 ∧ ∀𝑣𝑈𝑤𝑈 (𝑈 ∩ 𝒫 (𝑣𝑤)) ≠ ∅))))
4139, 40syl 17 . . . 4 (𝑈 ∈ (UnifOn‘𝑋) → (𝑈 ∈ (fBas‘(𝑋 × 𝑋)) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑈 ≠ ∅ ∧ ∅ ∉ 𝑈 ∧ ∀𝑣𝑈𝑤𝑈 (𝑈 ∩ 𝒫 (𝑣𝑤)) ≠ ∅))))
4241adantl 481 . . 3 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → (𝑈 ∈ (fBas‘(𝑋 × 𝑋)) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑈 ≠ ∅ ∧ ∅ ∉ 𝑈 ∧ ∀𝑣𝑈𝑤𝑈 (𝑈 ∩ 𝒫 (𝑣𝑤)) ≠ ∅))))
436, 38, 42mpbir2and 713 . 2 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → 𝑈 ∈ (fBas‘(𝑋 × 𝑋)))
44 n0 4352 . . . . 5 ((𝑈 ∩ 𝒫 𝑤) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ (𝑈 ∩ 𝒫 𝑤))
45 elin 3966 . . . . . . 7 (𝑣 ∈ (𝑈 ∩ 𝒫 𝑤) ↔ (𝑣𝑈𝑣 ∈ 𝒫 𝑤))
46 velpw 4604 . . . . . . . 8 (𝑣 ∈ 𝒫 𝑤𝑣𝑤)
4746anbi2i 623 . . . . . . 7 ((𝑣𝑈𝑣 ∈ 𝒫 𝑤) ↔ (𝑣𝑈𝑣𝑤))
4845, 47bitri 275 . . . . . 6 (𝑣 ∈ (𝑈 ∩ 𝒫 𝑤) ↔ (𝑣𝑈𝑣𝑤))
4948exbii 1847 . . . . 5 (∃𝑣 𝑣 ∈ (𝑈 ∩ 𝒫 𝑤) ↔ ∃𝑣(𝑣𝑈𝑣𝑤))
5044, 49bitri 275 . . . 4 ((𝑈 ∩ 𝒫 𝑤) ≠ ∅ ↔ ∃𝑣(𝑣𝑈𝑣𝑤))
5110simp1d 1142 . . . . . . . 8 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) → ∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣𝑤𝑤𝑈))
5251r19.21bi 3250 . . . . . . 7 ((((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣𝑈) ∧ 𝑤 ∈ 𝒫 (𝑋 × 𝑋)) → (𝑣𝑤𝑤𝑈))
5352an32s 652 . . . . . 6 ((((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑤 ∈ 𝒫 (𝑋 × 𝑋)) ∧ 𝑣𝑈) → (𝑣𝑤𝑤𝑈))
5453expimpd 453 . . . . 5 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑤 ∈ 𝒫 (𝑋 × 𝑋)) → ((𝑣𝑈𝑣𝑤) → 𝑤𝑈))
5554exlimdv 1932 . . . 4 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑤 ∈ 𝒫 (𝑋 × 𝑋)) → (∃𝑣(𝑣𝑈𝑣𝑤) → 𝑤𝑈))
5650, 55biimtrid 242 . . 3 (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑤 ∈ 𝒫 (𝑋 × 𝑋)) → ((𝑈 ∩ 𝒫 𝑤) ≠ ∅ → 𝑤𝑈))
5756ralrimiva 3145 . 2 ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → ∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)((𝑈 ∩ 𝒫 𝑤) ≠ ∅ → 𝑤𝑈))
58 isfil 23856 . 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 1778  wcel 2107  wne 2939  wnel 3045  wral 3060  wrex 3069  Vcvv 3479  cin 3949  wss 3950  c0 4332  𝒫 cpw 4599  cop 4631   I cid 5576   × cxp 5682  ccnv 5683  cres 5686  ccom 5688  cfv 6560  fBascfbas 21353  Filcfil 23854  UnifOncust 24209
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6513  df-fun 6562  df-fv 6568  df-fbas 21362  df-fil 23855  df-ust 24210
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator