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

Theorem ufinffr 23185
Description: An infinite subset is contained in a free ultrafilter. (Contributed by Jeff Hankins, 6-Dec-2009.) (Revised by Mario Carneiro, 4-Dec-2013.)
Assertion
Ref Expression
ufinffr ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ∃𝑓 ∈ (UFil‘𝑋)(𝐴𝑓 𝑓 = ∅))
Distinct variable groups:   𝐴,𝑓   𝐵,𝑓   𝑓,𝑋

Proof of Theorem ufinffr
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ominf 9127 . . . . 5 ¬ ω ∈ Fin
2 domfi 9061 . . . . . 6 ((𝐴 ∈ Fin ∧ ω ≼ 𝐴) → ω ∈ Fin)
32expcom 415 . . . . 5 (ω ≼ 𝐴 → (𝐴 ∈ Fin → ω ∈ Fin))
41, 3mtoi 198 . . . 4 (ω ≼ 𝐴 → ¬ 𝐴 ∈ Fin)
5 cfinfil 23149 . . . 4 ((𝑋𝐵𝐴𝑋 ∧ ¬ 𝐴 ∈ Fin) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ∈ (Fil‘𝑋))
64, 5syl3an3 1165 . . 3 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ∈ (Fil‘𝑋))
7 filssufil 23168 . . 3 ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋){𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ⊆ 𝑓)
86, 7syl 17 . 2 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ∃𝑓 ∈ (UFil‘𝑋){𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ⊆ 𝑓)
9 difeq2 4067 . . . . . . . 8 (𝑥 = 𝐴 → (𝐴𝑥) = (𝐴𝐴))
10 difid 4321 . . . . . . . 8 (𝐴𝐴) = ∅
119, 10eqtrdi 2793 . . . . . . 7 (𝑥 = 𝐴 → (𝐴𝑥) = ∅)
1211eleq1d 2822 . . . . . 6 (𝑥 = 𝐴 → ((𝐴𝑥) ∈ Fin ↔ ∅ ∈ Fin))
13 elpw2g 5292 . . . . . . . 8 (𝑋𝐵 → (𝐴 ∈ 𝒫 𝑋𝐴𝑋))
1413biimpar 479 . . . . . . 7 ((𝑋𝐵𝐴𝑋) → 𝐴 ∈ 𝒫 𝑋)
15143adant3 1132 . . . . . 6 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → 𝐴 ∈ 𝒫 𝑋)
16 0fin 9040 . . . . . . 7 ∅ ∈ Fin
1716a1i 11 . . . . . 6 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ∅ ∈ Fin)
1812, 15, 17elrabd 3639 . . . . 5 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → 𝐴 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin})
19 ssel 3928 . . . . 5 ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ⊆ 𝑓 → (𝐴 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} → 𝐴𝑓))
2018, 19syl5com 31 . . . 4 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ⊆ 𝑓𝐴𝑓))
21 intss 4921 . . . . . 6 ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ⊆ 𝑓 𝑓 {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin})
22 neldifsn 4743 . . . . . . . . . 10 ¬ 𝑦 ∈ (𝐴 ∖ {𝑦})
23 elinti 4907 . . . . . . . . . 10 (𝑦 {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} → ((𝐴 ∖ {𝑦}) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} → 𝑦 ∈ (𝐴 ∖ {𝑦})))
2422, 23mtoi 198 . . . . . . . . 9 (𝑦 {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} → ¬ (𝐴 ∖ {𝑦}) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin})
25 difeq2 4067 . . . . . . . . . . 11 (𝑥 = (𝐴 ∖ {𝑦}) → (𝐴𝑥) = (𝐴 ∖ (𝐴 ∖ {𝑦})))
2625eleq1d 2822 . . . . . . . . . 10 (𝑥 = (𝐴 ∖ {𝑦}) → ((𝐴𝑥) ∈ Fin ↔ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
27 simp2 1137 . . . . . . . . . . . 12 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → 𝐴𝑋)
2827ssdifssd 4093 . . . . . . . . . . 11 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → (𝐴 ∖ {𝑦}) ⊆ 𝑋)
29 elpw2g 5292 . . . . . . . . . . . 12 (𝑋𝐵 → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝑋 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝑋))
30293ad2ant1 1133 . . . . . . . . . . 11 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝑋 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝑋))
3128, 30mpbird 257 . . . . . . . . . 10 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → (𝐴 ∖ {𝑦}) ∈ 𝒫 𝑋)
32 snfi 8913 . . . . . . . . . . . 12 {𝑦} ∈ Fin
33 eldif 3911 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴 ∖ (𝐴 ∖ {𝑦})) ↔ (𝑥𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∖ {𝑦})))
34 eldif 3911 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴 ∖ {𝑦}) ↔ (𝑥𝐴 ∧ ¬ 𝑥 ∈ {𝑦}))
3534notbii 320 . . . . . . . . . . . . . . . . 17 𝑥 ∈ (𝐴 ∖ {𝑦}) ↔ ¬ (𝑥𝐴 ∧ ¬ 𝑥 ∈ {𝑦}))
36 iman 403 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴𝑥 ∈ {𝑦}) ↔ ¬ (𝑥𝐴 ∧ ¬ 𝑥 ∈ {𝑦}))
3735, 36bitr4i 278 . . . . . . . . . . . . . . . 16 𝑥 ∈ (𝐴 ∖ {𝑦}) ↔ (𝑥𝐴𝑥 ∈ {𝑦}))
3837anbi2i 624 . . . . . . . . . . . . . . 15 ((𝑥𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∖ {𝑦})) ↔ (𝑥𝐴 ∧ (𝑥𝐴𝑥 ∈ {𝑦})))
3933, 38bitri 275 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴 ∖ (𝐴 ∖ {𝑦})) ↔ (𝑥𝐴 ∧ (𝑥𝐴𝑥 ∈ {𝑦})))
40 pm3.35 801 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ (𝑥𝐴𝑥 ∈ {𝑦})) → 𝑥 ∈ {𝑦})
4139, 40sylbi 216 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴 ∖ (𝐴 ∖ {𝑦})) → 𝑥 ∈ {𝑦})
4241ssriv 3939 . . . . . . . . . . . 12 (𝐴 ∖ (𝐴 ∖ {𝑦})) ⊆ {𝑦}
43 ssfi 9042 . . . . . . . . . . . 12 (({𝑦} ∈ Fin ∧ (𝐴 ∖ (𝐴 ∖ {𝑦})) ⊆ {𝑦}) → (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin)
4432, 42, 43mp2an 690 . . . . . . . . . . 11 (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin
4544a1i 11 . . . . . . . . . 10 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin)
4626, 31, 45elrabd 3639 . . . . . . . . 9 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → (𝐴 ∖ {𝑦}) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin})
4724, 46nsyl3 138 . . . . . . . 8 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ¬ 𝑦 {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin})
4847eq0rdv 4355 . . . . . . 7 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} = ∅)
4948sseq2d 3967 . . . . . 6 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ( 𝑓 {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ↔ 𝑓 ⊆ ∅))
5021, 49syl5ib 244 . . . . 5 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ⊆ 𝑓 𝑓 ⊆ ∅))
51 ss0 4349 . . . . 5 ( 𝑓 ⊆ ∅ → 𝑓 = ∅)
5250, 51syl6 35 . . . 4 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ⊆ 𝑓 𝑓 = ∅))
5320, 52jcad 514 . . 3 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ⊆ 𝑓 → (𝐴𝑓 𝑓 = ∅)))
5453reximdv 3164 . 2 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → (∃𝑓 ∈ (UFil‘𝑋){𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ⊆ 𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐴𝑓 𝑓 = ∅)))
558, 54mpd 15 1 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ∃𝑓 ∈ (UFil‘𝑋)(𝐴𝑓 𝑓 = ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  w3a 1087   = wceq 1541  wcel 2106  wrex 3071  {crab 3404  cdif 3898  wss 3901  c0 4273  𝒫 cpw 4551  {csn 4577   cint 4898   class class class wbr 5096  cfv 6483  ωcom 7784  cdom 8806  Fincfn 8808  Filcfil 23101  UFilcufil 23155
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5233  ax-sep 5247  ax-nul 5254  ax-pow 5312  ax-pr 5376  ax-un 7654  ax-ac2 10324
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3731  df-csb 3847  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3920  df-nul 4274  df-if 4478  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4857  df-int 4899  df-iun 4947  df-br 5097  df-opab 5159  df-mpt 5180  df-tr 5214  df-id 5522  df-eprel 5528  df-po 5536  df-so 5537  df-fr 5579  df-se 5580  df-we 5581  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6242  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6435  df-fun 6485  df-fn 6486  df-f 6487  df-f1 6488  df-fo 6489  df-f1o 6490  df-fv 6491  df-isom 6492  df-riota 7297  df-ov 7344  df-oprab 7345  df-mpo 7346  df-rpss 7642  df-om 7785  df-1st 7903  df-2nd 7904  df-frecs 8171  df-wrecs 8202  df-recs 8276  df-rdg 8315  df-1o 8371  df-oadd 8375  df-er 8573  df-en 8809  df-dom 8810  df-sdom 8811  df-fin 8812  df-fi 9272  df-dju 9762  df-card 9800  df-ac 9977  df-fbas 20699  df-fg 20700  df-fil 23102  df-ufil 23157
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator