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

Theorem isfin1-3 10329
Description: A set is I-finite iff every system of subsets contains a maximal subset. Definition I of [Levy58] p. 2. (Contributed by Stefan O'Rear, 4-Nov-2014.) (Proof shortened by Mario Carneiro, 17-May-2015.)
Assertion
Ref Expression
isfin1-3 (𝐴𝑉 → (𝐴 ∈ Fin ↔ [] Fr 𝒫 𝐴))

Proof of Theorem isfin1-3
Dummy variables 𝑏 𝑐 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 porpss 7669 . . . 4 [] Po 𝒫 𝐴
2 cnvpo 6244 . . . 4 ( [] Po 𝒫 𝐴 [] Po 𝒫 𝐴)
31, 2mpbi 229 . . 3 [] Po 𝒫 𝐴
4 pwfi 9129 . . . 4 (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin)
54biimpi 215 . . 3 (𝐴 ∈ Fin → 𝒫 𝐴 ∈ Fin)
6 frfi 9239 . . 3 (( [] Po 𝒫 𝐴 ∧ 𝒫 𝐴 ∈ Fin) → [] Fr 𝒫 𝐴)
73, 5, 6sylancr 588 . 2 (𝐴 ∈ Fin → [] Fr 𝒫 𝐴)
8 inss2 4194 . . . . . 6 (Fin ∩ 𝒫 𝐴) ⊆ 𝒫 𝐴
9 pwexg 5338 . . . . . 6 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
10 ssexg 5285 . . . . . 6 (((Fin ∩ 𝒫 𝐴) ⊆ 𝒫 𝐴 ∧ 𝒫 𝐴 ∈ V) → (Fin ∩ 𝒫 𝐴) ∈ V)
118, 9, 10sylancr 588 . . . . 5 (𝐴𝑉 → (Fin ∩ 𝒫 𝐴) ∈ V)
12 0fin 9122 . . . . . . . 8 ∅ ∈ Fin
13 0elpw 5316 . . . . . . . 8 ∅ ∈ 𝒫 𝐴
1412, 13elini 4158 . . . . . . 7 ∅ ∈ (Fin ∩ 𝒫 𝐴)
1514ne0ii 4302 . . . . . 6 (Fin ∩ 𝒫 𝐴) ≠ ∅
16 fri 5598 . . . . . 6 ((((Fin ∩ 𝒫 𝐴) ∈ V ∧ [] Fr 𝒫 𝐴) ∧ ((Fin ∩ 𝒫 𝐴) ⊆ 𝒫 𝐴 ∧ (Fin ∩ 𝒫 𝐴) ≠ ∅)) → ∃𝑏 ∈ (Fin ∩ 𝒫 𝐴)∀𝑐 ∈ (Fin ∩ 𝒫 𝐴) ¬ 𝑐 [] 𝑏)
178, 15, 16mpanr12 704 . . . . 5 (((Fin ∩ 𝒫 𝐴) ∈ V ∧ [] Fr 𝒫 𝐴) → ∃𝑏 ∈ (Fin ∩ 𝒫 𝐴)∀𝑐 ∈ (Fin ∩ 𝒫 𝐴) ¬ 𝑐 [] 𝑏)
1811, 17sylan 581 . . . 4 ((𝐴𝑉 [] Fr 𝒫 𝐴) → ∃𝑏 ∈ (Fin ∩ 𝒫 𝐴)∀𝑐 ∈ (Fin ∩ 𝒫 𝐴) ¬ 𝑐 [] 𝑏)
1918ex 414 . . 3 (𝐴𝑉 → ( [] Fr 𝒫 𝐴 → ∃𝑏 ∈ (Fin ∩ 𝒫 𝐴)∀𝑐 ∈ (Fin ∩ 𝒫 𝐴) ¬ 𝑐 [] 𝑏))
20 elinel1 4160 . . . . 5 (𝑏 ∈ (Fin ∩ 𝒫 𝐴) → 𝑏 ∈ Fin)
21 ralnex 3076 . . . . . . . 8 (∀𝑐 ∈ (Fin ∩ 𝒫 𝐴) ¬ 𝑐 [] 𝑏 ↔ ¬ ∃𝑐 ∈ (Fin ∩ 𝒫 𝐴)𝑐 [] 𝑏)
2220adantr 482 . . . . . . . . . . . . 13 ((𝑏 ∈ (Fin ∩ 𝒫 𝐴) ∧ (𝑑𝐴 ∧ ¬ 𝑑𝑏)) → 𝑏 ∈ Fin)
23 snfi 8995 . . . . . . . . . . . . 13 {𝑑} ∈ Fin
24 unfi 9123 . . . . . . . . . . . . 13 ((𝑏 ∈ Fin ∧ {𝑑} ∈ Fin) → (𝑏 ∪ {𝑑}) ∈ Fin)
2522, 23, 24sylancl 587 . . . . . . . . . . . 12 ((𝑏 ∈ (Fin ∩ 𝒫 𝐴) ∧ (𝑑𝐴 ∧ ¬ 𝑑𝑏)) → (𝑏 ∪ {𝑑}) ∈ Fin)
26 elinel2 4161 . . . . . . . . . . . . . . . 16 (𝑏 ∈ (Fin ∩ 𝒫 𝐴) → 𝑏 ∈ 𝒫 𝐴)
2726elpwid 4574 . . . . . . . . . . . . . . 15 (𝑏 ∈ (Fin ∩ 𝒫 𝐴) → 𝑏𝐴)
2827adantr 482 . . . . . . . . . . . . . 14 ((𝑏 ∈ (Fin ∩ 𝒫 𝐴) ∧ (𝑑𝐴 ∧ ¬ 𝑑𝑏)) → 𝑏𝐴)
29 snssi 4773 . . . . . . . . . . . . . . 15 (𝑑𝐴 → {𝑑} ⊆ 𝐴)
3029ad2antrl 727 . . . . . . . . . . . . . 14 ((𝑏 ∈ (Fin ∩ 𝒫 𝐴) ∧ (𝑑𝐴 ∧ ¬ 𝑑𝑏)) → {𝑑} ⊆ 𝐴)
3128, 30unssd 4151 . . . . . . . . . . . . 13 ((𝑏 ∈ (Fin ∩ 𝒫 𝐴) ∧ (𝑑𝐴 ∧ ¬ 𝑑𝑏)) → (𝑏 ∪ {𝑑}) ⊆ 𝐴)
32 vex 3452 . . . . . . . . . . . . . . 15 𝑏 ∈ V
33 vsnex 5391 . . . . . . . . . . . . . . 15 {𝑑} ∈ V
3432, 33unex 7685 . . . . . . . . . . . . . 14 (𝑏 ∪ {𝑑}) ∈ V
3534elpw 4569 . . . . . . . . . . . . 13 ((𝑏 ∪ {𝑑}) ∈ 𝒫 𝐴 ↔ (𝑏 ∪ {𝑑}) ⊆ 𝐴)
3631, 35sylibr 233 . . . . . . . . . . . 12 ((𝑏 ∈ (Fin ∩ 𝒫 𝐴) ∧ (𝑑𝐴 ∧ ¬ 𝑑𝑏)) → (𝑏 ∪ {𝑑}) ∈ 𝒫 𝐴)
3725, 36elind 4159 . . . . . . . . . . 11 ((𝑏 ∈ (Fin ∩ 𝒫 𝐴) ∧ (𝑑𝐴 ∧ ¬ 𝑑𝑏)) → (𝑏 ∪ {𝑑}) ∈ (Fin ∩ 𝒫 𝐴))
38 disjsn 4677 . . . . . . . . . . . . . . 15 ((𝑏 ∩ {𝑑}) = ∅ ↔ ¬ 𝑑𝑏)
3938biimpri 227 . . . . . . . . . . . . . 14 𝑑𝑏 → (𝑏 ∩ {𝑑}) = ∅)
40 vex 3452 . . . . . . . . . . . . . . 15 𝑑 ∈ V
4140snnz 4742 . . . . . . . . . . . . . 14 {𝑑} ≠ ∅
42 disjpss 4425 . . . . . . . . . . . . . 14 (((𝑏 ∩ {𝑑}) = ∅ ∧ {𝑑} ≠ ∅) → 𝑏 ⊊ (𝑏 ∪ {𝑑}))
4339, 41, 42sylancl 587 . . . . . . . . . . . . 13 𝑑𝑏𝑏 ⊊ (𝑏 ∪ {𝑑}))
4443ad2antll 728 . . . . . . . . . . . 12 ((𝑏 ∈ (Fin ∩ 𝒫 𝐴) ∧ (𝑑𝐴 ∧ ¬ 𝑑𝑏)) → 𝑏 ⊊ (𝑏 ∪ {𝑑}))
4534, 32brcnv 5843 . . . . . . . . . . . . 13 ((𝑏 ∪ {𝑑}) [] 𝑏𝑏 [] (𝑏 ∪ {𝑑}))
4634brrpss 7668 . . . . . . . . . . . . 13 (𝑏 [] (𝑏 ∪ {𝑑}) ↔ 𝑏 ⊊ (𝑏 ∪ {𝑑}))
4745, 46bitri 275 . . . . . . . . . . . 12 ((𝑏 ∪ {𝑑}) [] 𝑏𝑏 ⊊ (𝑏 ∪ {𝑑}))
4844, 47sylibr 233 . . . . . . . . . . 11 ((𝑏 ∈ (Fin ∩ 𝒫 𝐴) ∧ (𝑑𝐴 ∧ ¬ 𝑑𝑏)) → (𝑏 ∪ {𝑑}) [] 𝑏)
49 breq1 5113 . . . . . . . . . . . 12 (𝑐 = (𝑏 ∪ {𝑑}) → (𝑐 [] 𝑏 ↔ (𝑏 ∪ {𝑑}) [] 𝑏))
5049rspcev 3584 . . . . . . . . . . 11 (((𝑏 ∪ {𝑑}) ∈ (Fin ∩ 𝒫 𝐴) ∧ (𝑏 ∪ {𝑑}) [] 𝑏) → ∃𝑐 ∈ (Fin ∩ 𝒫 𝐴)𝑐 [] 𝑏)
5137, 48, 50syl2anc 585 . . . . . . . . . 10 ((𝑏 ∈ (Fin ∩ 𝒫 𝐴) ∧ (𝑑𝐴 ∧ ¬ 𝑑𝑏)) → ∃𝑐 ∈ (Fin ∩ 𝒫 𝐴)𝑐 [] 𝑏)
5251expr 458 . . . . . . . . 9 ((𝑏 ∈ (Fin ∩ 𝒫 𝐴) ∧ 𝑑𝐴) → (¬ 𝑑𝑏 → ∃𝑐 ∈ (Fin ∩ 𝒫 𝐴)𝑐 [] 𝑏))
5352con1d 145 . . . . . . . 8 ((𝑏 ∈ (Fin ∩ 𝒫 𝐴) ∧ 𝑑𝐴) → (¬ ∃𝑐 ∈ (Fin ∩ 𝒫 𝐴)𝑐 [] 𝑏𝑑𝑏))
5421, 53biimtrid 241 . . . . . . 7 ((𝑏 ∈ (Fin ∩ 𝒫 𝐴) ∧ 𝑑𝐴) → (∀𝑐 ∈ (Fin ∩ 𝒫 𝐴) ¬ 𝑐 [] 𝑏𝑑𝑏))
5554impancom 453 . . . . . 6 ((𝑏 ∈ (Fin ∩ 𝒫 𝐴) ∧ ∀𝑐 ∈ (Fin ∩ 𝒫 𝐴) ¬ 𝑐 [] 𝑏) → (𝑑𝐴𝑑𝑏))
5655ssrdv 3955 . . . . 5 ((𝑏 ∈ (Fin ∩ 𝒫 𝐴) ∧ ∀𝑐 ∈ (Fin ∩ 𝒫 𝐴) ¬ 𝑐 [] 𝑏) → 𝐴𝑏)
57 ssfi 9124 . . . . 5 ((𝑏 ∈ Fin ∧ 𝐴𝑏) → 𝐴 ∈ Fin)
5820, 56, 57syl2an2r 684 . . . 4 ((𝑏 ∈ (Fin ∩ 𝒫 𝐴) ∧ ∀𝑐 ∈ (Fin ∩ 𝒫 𝐴) ¬ 𝑐 [] 𝑏) → 𝐴 ∈ Fin)
5958rexlimiva 3145 . . 3 (∃𝑏 ∈ (Fin ∩ 𝒫 𝐴)∀𝑐 ∈ (Fin ∩ 𝒫 𝐴) ¬ 𝑐 [] 𝑏𝐴 ∈ Fin)
6019, 59syl6 35 . 2 (𝐴𝑉 → ( [] Fr 𝒫 𝐴𝐴 ∈ Fin))
617, 60impbid2 225 1 (𝐴𝑉 → (𝐴 ∈ Fin ↔ [] Fr 𝒫 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wne 2944  wral 3065  wrex 3074  Vcvv 3448  cun 3913  cin 3914  wss 3915  wpss 3916  c0 4287  𝒫 cpw 4565  {csn 4591   class class class wbr 5110   Po wpo 5548   Fr wfr 5590  ccnv 5637   [] crpss 7664  Fincfn 8890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-rpss 7665  df-om 7808  df-1o 8417  df-en 8891  df-fin 8894
This theorem is referenced by:  isfin1-4  10330  fin12  10356
  Copyright terms: Public domain W3C validator