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

Theorem ufinffr 21643
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 8116 . . . . 5 ¬ ω ∈ Fin
2 domfi 8125 . . . . . 6 ((𝐴 ∈ Fin ∧ ω ≼ 𝐴) → ω ∈ Fin)
32expcom 451 . . . . 5 (ω ≼ 𝐴 → (𝐴 ∈ Fin → ω ∈ Fin))
41, 3mtoi 190 . . . 4 (ω ≼ 𝐴 → ¬ 𝐴 ∈ Fin)
5 cfinfil 21607 . . . 4 ((𝑋𝐵𝐴𝑋 ∧ ¬ 𝐴 ∈ Fin) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ∈ (Fil‘𝑋))
64, 5syl3an3 1358 . . 3 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ∈ (Fil‘𝑋))
7 filssufil 21626 . . 3 ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋){𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ⊆ 𝑓)
86, 7syl 17 . 2 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ∃𝑓 ∈ (UFil‘𝑋){𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ⊆ 𝑓)
9 elpw2g 4787 . . . . . . . 8 (𝑋𝐵 → (𝐴 ∈ 𝒫 𝑋𝐴𝑋))
109biimpar 502 . . . . . . 7 ((𝑋𝐵𝐴𝑋) → 𝐴 ∈ 𝒫 𝑋)
11103adant3 1079 . . . . . 6 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → 𝐴 ∈ 𝒫 𝑋)
12 0fin 8132 . . . . . . 7 ∅ ∈ Fin
1312a1i 11 . . . . . 6 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ∅ ∈ Fin)
14 difeq2 3700 . . . . . . . . 9 (𝑥 = 𝐴 → (𝐴𝑥) = (𝐴𝐴))
15 difid 3922 . . . . . . . . 9 (𝐴𝐴) = ∅
1614, 15syl6eq 2671 . . . . . . . 8 (𝑥 = 𝐴 → (𝐴𝑥) = ∅)
1716eleq1d 2683 . . . . . . 7 (𝑥 = 𝐴 → ((𝐴𝑥) ∈ Fin ↔ ∅ ∈ Fin))
1817elrab 3346 . . . . . 6 (𝐴 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ↔ (𝐴 ∈ 𝒫 𝑋 ∧ ∅ ∈ Fin))
1911, 13, 18sylanbrc 697 . . . . 5 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → 𝐴 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin})
20 ssel 3577 . . . . 5 ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ⊆ 𝑓 → (𝐴 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} → 𝐴𝑓))
2119, 20syl5com 31 . . . 4 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ⊆ 𝑓𝐴𝑓))
22 intss 4463 . . . . . 6 ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ⊆ 𝑓 𝑓 {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin})
23 neldifsn 4290 . . . . . . . . . 10 ¬ 𝑦 ∈ (𝐴 ∖ {𝑦})
24 elinti 4450 . . . . . . . . . 10 (𝑦 {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} → ((𝐴 ∖ {𝑦}) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} → 𝑦 ∈ (𝐴 ∖ {𝑦})))
2523, 24mtoi 190 . . . . . . . . 9 (𝑦 {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} → ¬ (𝐴 ∖ {𝑦}) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin})
26 simp2 1060 . . . . . . . . . . . 12 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → 𝐴𝑋)
2726ssdifssd 3726 . . . . . . . . . . 11 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → (𝐴 ∖ {𝑦}) ⊆ 𝑋)
28 elpw2g 4787 . . . . . . . . . . . 12 (𝑋𝐵 → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝑋 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝑋))
29283ad2ant1 1080 . . . . . . . . . . 11 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝑋 ↔ (𝐴 ∖ {𝑦}) ⊆ 𝑋))
3027, 29mpbird 247 . . . . . . . . . 10 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → (𝐴 ∖ {𝑦}) ∈ 𝒫 𝑋)
31 snfi 7982 . . . . . . . . . . . 12 {𝑦} ∈ Fin
32 eldif 3565 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴 ∖ (𝐴 ∖ {𝑦})) ↔ (𝑥𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∖ {𝑦})))
33 eldif 3565 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴 ∖ {𝑦}) ↔ (𝑥𝐴 ∧ ¬ 𝑥 ∈ {𝑦}))
3433notbii 310 . . . . . . . . . . . . . . . . 17 𝑥 ∈ (𝐴 ∖ {𝑦}) ↔ ¬ (𝑥𝐴 ∧ ¬ 𝑥 ∈ {𝑦}))
35 iman 440 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴𝑥 ∈ {𝑦}) ↔ ¬ (𝑥𝐴 ∧ ¬ 𝑥 ∈ {𝑦}))
3634, 35bitr4i 267 . . . . . . . . . . . . . . . 16 𝑥 ∈ (𝐴 ∖ {𝑦}) ↔ (𝑥𝐴𝑥 ∈ {𝑦}))
3736anbi2i 729 . . . . . . . . . . . . . . 15 ((𝑥𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∖ {𝑦})) ↔ (𝑥𝐴 ∧ (𝑥𝐴𝑥 ∈ {𝑦})))
3832, 37bitri 264 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴 ∖ (𝐴 ∖ {𝑦})) ↔ (𝑥𝐴 ∧ (𝑥𝐴𝑥 ∈ {𝑦})))
39 pm3.35 610 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ (𝑥𝐴𝑥 ∈ {𝑦})) → 𝑥 ∈ {𝑦})
4038, 39sylbi 207 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴 ∖ (𝐴 ∖ {𝑦})) → 𝑥 ∈ {𝑦})
4140ssriv 3587 . . . . . . . . . . . 12 (𝐴 ∖ (𝐴 ∖ {𝑦})) ⊆ {𝑦}
42 ssfi 8124 . . . . . . . . . . . 12 (({𝑦} ∈ Fin ∧ (𝐴 ∖ (𝐴 ∖ {𝑦})) ⊆ {𝑦}) → (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin)
4331, 41, 42mp2an 707 . . . . . . . . . . 11 (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin
4443a1i 11 . . . . . . . . . 10 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin)
45 difeq2 3700 . . . . . . . . . . . 12 (𝑥 = (𝐴 ∖ {𝑦}) → (𝐴𝑥) = (𝐴 ∖ (𝐴 ∖ {𝑦})))
4645eleq1d 2683 . . . . . . . . . . 11 (𝑥 = (𝐴 ∖ {𝑦}) → ((𝐴𝑥) ∈ Fin ↔ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
4746elrab 3346 . . . . . . . . . 10 ((𝐴 ∖ {𝑦}) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ↔ ((𝐴 ∖ {𝑦}) ∈ 𝒫 𝑋 ∧ (𝐴 ∖ (𝐴 ∖ {𝑦})) ∈ Fin))
4830, 44, 47sylanbrc 697 . . . . . . . . 9 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → (𝐴 ∖ {𝑦}) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin})
4925, 48nsyl3 133 . . . . . . . 8 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ¬ 𝑦 {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin})
5049eq0rdv 3951 . . . . . . 7 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} = ∅)
5150sseq2d 3612 . . . . . 6 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ( 𝑓 {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ↔ 𝑓 ⊆ ∅))
5222, 51syl5ib 234 . . . . 5 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ⊆ 𝑓 𝑓 ⊆ ∅))
53 ss0 3946 . . . . 5 ( 𝑓 ⊆ ∅ → 𝑓 = ∅)
5452, 53syl6 35 . . . 4 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ⊆ 𝑓 𝑓 = ∅))
5521, 54jcad 555 . . 3 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ({𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ⊆ 𝑓 → (𝐴𝑓 𝑓 = ∅)))
5655reximdv 3010 . 2 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → (∃𝑓 ∈ (UFil‘𝑋){𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥) ∈ Fin} ⊆ 𝑓 → ∃𝑓 ∈ (UFil‘𝑋)(𝐴𝑓 𝑓 = ∅)))
578, 56mpd 15 1 ((𝑋𝐵𝐴𝑋 ∧ ω ≼ 𝐴) → ∃𝑓 ∈ (UFil‘𝑋)(𝐴𝑓 𝑓 = ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wrex 2908  {crab 2911  cdif 3552  wss 3555  c0 3891  𝒫 cpw 4130  {csn 4148   cint 4440   class class class wbr 4613  cfv 5847  ωcom 7012  cdom 7897  Fincfn 7899  Filcfil 21559  UFilcufil 21613
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-ac2 9229
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-rpss 6890  df-om 7013  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-fi 8261  df-card 8709  df-ac 8883  df-cda 8934  df-fbas 19662  df-fg 19663  df-fil 21560  df-ufil 21615
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator