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

Theorem isfin1-3 8797
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  |-  ( A  e.  V  ->  ( A  e.  Fin  <->  `' [ C.]  Fr  ~P A ) )

Proof of Theorem isfin1-3
Dummy variables  b 
c  d are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 porpss 6565 . . . 4  |- [ C.]  Po  ~P A
2 cnvpo 5361 . . . 4  |-  ( [ C.]  Po  ~P A  <->  `' [ C.]  Po  ~P A )
31, 2mpbi 208 . . 3  |-  `' [ C.]  Po  ~P A
4 pwfi 7848 . . . 4  |-  ( A  e.  Fin  <->  ~P A  e.  Fin )
54biimpi 194 . . 3  |-  ( A  e.  Fin  ->  ~P A  e.  Fin )
6 frfi 7798 . . 3  |-  ( ( `' [ C.]  Po  ~P A  /\  ~P A  e.  Fin )  ->  `' [ C.]  Fr  ~P A )
73, 5, 6sylancr 661 . 2  |-  ( A  e.  Fin  ->  `' [ C.] 
Fr  ~P A )
8 inss2 3659 . . . . . 6  |-  ( Fin 
i^i  ~P A )  C_  ~P A
9 pwexg 4577 . . . . . 6  |-  ( A  e.  V  ->  ~P A  e.  _V )
10 ssexg 4539 . . . . . 6  |-  ( ( ( Fin  i^i  ~P A )  C_  ~P A  /\  ~P A  e. 
_V )  ->  ( Fin  i^i  ~P A )  e.  _V )
118, 9, 10sylancr 661 . . . . 5  |-  ( A  e.  V  ->  ( Fin  i^i  ~P A )  e.  _V )
12 0fin 7781 . . . . . . . 8  |-  (/)  e.  Fin
13 0elpw 4562 . . . . . . . 8  |-  (/)  e.  ~P A
14 elin 3625 . . . . . . . 8  |-  ( (/)  e.  ( Fin  i^i  ~P A )  <->  ( (/)  e.  Fin  /\  (/)  e.  ~P A ) )
1512, 13, 14mpbir2an 921 . . . . . . 7  |-  (/)  e.  ( Fin  i^i  ~P A
)
1615ne0ii 3744 . . . . . 6  |-  ( Fin 
i^i  ~P A )  =/=  (/)
17 fri 4784 . . . . . 6  |-  ( ( ( ( Fin  i^i  ~P A )  e.  _V  /\  `' [ C.]  Fr  ~P A
)  /\  ( ( Fin  i^i  ~P A ) 
C_  ~P A  /\  ( Fin  i^i  ~P A )  =/=  (/) ) )  ->  E. b  e.  ( Fin  i^i  ~P A ) A. c  e.  ( Fin  i^i  ~P A
)  -.  c `' [ C.]  b )
188, 16, 17mpanr12 683 . . . . 5  |-  ( ( ( Fin  i^i  ~P A )  e.  _V  /\  `' [ C.]  Fr  ~P A
)  ->  E. b  e.  ( Fin  i^i  ~P A ) A. c  e.  ( Fin  i^i  ~P A )  -.  c `' [ C.]  b )
1911, 18sylan 469 . . . 4  |-  ( ( A  e.  V  /\  `' [ C.]  Fr  ~P A
)  ->  E. b  e.  ( Fin  i^i  ~P A ) A. c  e.  ( Fin  i^i  ~P A )  -.  c `' [ C.]  b )
2019ex 432 . . 3  |-  ( A  e.  V  ->  ( `' [ C.]  Fr  ~P A  ->  E. b  e.  ( Fin  i^i  ~P A
) A. c  e.  ( Fin  i^i  ~P A )  -.  c `' [ C.]  b ) )
21 inss1 3658 . . . . . 6  |-  ( Fin 
i^i  ~P A )  C_  Fin
22 simpl 455 . . . . . 6  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  A. c  e.  ( Fin 
i^i  ~P A )  -.  c `' [ C.]  b
)  ->  b  e.  ( Fin  i^i  ~P A
) )
2321, 22sseldi 3439 . . . . 5  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  A. c  e.  ( Fin 
i^i  ~P A )  -.  c `' [ C.]  b
)  ->  b  e.  Fin )
24 ralnex 2849 . . . . . . . 8  |-  ( A. c  e.  ( Fin  i^i 
~P A )  -.  c `' [ C.]  b  <->  -. 
E. c  e.  ( Fin  i^i  ~P A
) c `' [ C.]  b
)
2521sseli 3437 . . . . . . . . . . . . . 14  |-  ( b  e.  ( Fin  i^i  ~P A )  ->  b  e.  Fin )
2625adantr 463 . . . . . . . . . . . . 13  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  ( d  e.  A  /\  -.  d  e.  b ) )  ->  b  e.  Fin )
27 snfi 7633 . . . . . . . . . . . . 13  |-  { d }  e.  Fin
28 unfi 7820 . . . . . . . . . . . . 13  |-  ( ( b  e.  Fin  /\  { d }  e.  Fin )  ->  ( b  u. 
{ d } )  e.  Fin )
2926, 27, 28sylancl 660 . . . . . . . . . . . 12  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  ( d  e.  A  /\  -.  d  e.  b ) )  ->  (
b  u.  { d } )  e.  Fin )
30 elin 3625 . . . . . . . . . . . . . . . . 17  |-  ( b  e.  ( Fin  i^i  ~P A )  <->  ( b  e.  Fin  /\  b  e. 
~P A ) )
3130simprbi 462 . . . . . . . . . . . . . . . 16  |-  ( b  e.  ( Fin  i^i  ~P A )  ->  b  e.  ~P A )
3231elpwid 3964 . . . . . . . . . . . . . . 15  |-  ( b  e.  ( Fin  i^i  ~P A )  ->  b  C_  A )
3332adantr 463 . . . . . . . . . . . . . 14  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  ( d  e.  A  /\  -.  d  e.  b ) )  ->  b  C_  A )
34 snssi 4115 . . . . . . . . . . . . . . 15  |-  ( d  e.  A  ->  { d }  C_  A )
3534ad2antrl 726 . . . . . . . . . . . . . 14  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  ( d  e.  A  /\  -.  d  e.  b ) )  ->  { d }  C_  A )
3633, 35unssd 3618 . . . . . . . . . . . . 13  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  ( d  e.  A  /\  -.  d  e.  b ) )  ->  (
b  u.  { d } )  C_  A
)
37 vex 3061 . . . . . . . . . . . . . . 15  |-  b  e. 
_V
38 snex 4631 . . . . . . . . . . . . . . 15  |-  { d }  e.  _V
3937, 38unex 6579 . . . . . . . . . . . . . 14  |-  ( b  u.  { d } )  e.  _V
4039elpw 3960 . . . . . . . . . . . . 13  |-  ( ( b  u.  { d } )  e.  ~P A 
<->  ( b  u.  {
d } )  C_  A )
4136, 40sylibr 212 . . . . . . . . . . . 12  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  ( d  e.  A  /\  -.  d  e.  b ) )  ->  (
b  u.  { d } )  e.  ~P A )
4229, 41elind 3626 . . . . . . . . . . 11  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  ( d  e.  A  /\  -.  d  e.  b ) )  ->  (
b  u.  { d } )  e.  ( Fin  i^i  ~P A
) )
43 disjsn 4031 . . . . . . . . . . . . . . 15  |-  ( ( b  i^i  { d } )  =  (/)  <->  -.  d  e.  b )
4443biimpri 206 . . . . . . . . . . . . . 14  |-  ( -.  d  e.  b  -> 
( b  i^i  {
d } )  =  (/) )
45 vex 3061 . . . . . . . . . . . . . . 15  |-  d  e. 
_V
4645snnz 4089 . . . . . . . . . . . . . 14  |-  { d }  =/=  (/)
47 disjpss 3819 . . . . . . . . . . . . . 14  |-  ( ( ( b  i^i  {
d } )  =  (/)  /\  { d }  =/=  (/) )  ->  b  C.  ( b  u.  {
d } ) )
4844, 46, 47sylancl 660 . . . . . . . . . . . . 13  |-  ( -.  d  e.  b  -> 
b  C.  ( b  u.  { d } ) )
4948ad2antll 727 . . . . . . . . . . . 12  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  ( d  e.  A  /\  -.  d  e.  b ) )  ->  b  C.  ( b  u.  {
d } ) )
5039, 37brcnv 5005 . . . . . . . . . . . . 13  |-  ( ( b  u.  { d } ) `' [ C.]  b  <->  b [ C.]  ( b  u.  {
d } ) )
5139brrpss 6564 . . . . . . . . . . . . 13  |-  ( b [ C.]  ( b  u.  {
d } )  <->  b  C.  (
b  u.  { d } ) )
5250, 51bitri 249 . . . . . . . . . . . 12  |-  ( ( b  u.  { d } ) `' [ C.]  b  <->  b 
C.  ( b  u. 
{ d } ) )
5349, 52sylibr 212 . . . . . . . . . . 11  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  ( d  e.  A  /\  -.  d  e.  b ) )  ->  (
b  u.  { d } ) `' [ C.]  b
)
54 breq1 4397 . . . . . . . . . . . 12  |-  ( c  =  ( b  u. 
{ d } )  ->  ( c `' [ C.]  b  <->  ( b  u. 
{ d } ) `' [ C.]  b ) )
5554rspcev 3159 . . . . . . . . . . 11  |-  ( ( ( b  u.  {
d } )  e.  ( Fin  i^i  ~P A )  /\  (
b  u.  { d } ) `' [ C.]  b
)  ->  E. c  e.  ( Fin  i^i  ~P A ) c `' [ C.]  b )
5642, 53, 55syl2anc 659 . . . . . . . . . 10  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  ( d  e.  A  /\  -.  d  e.  b ) )  ->  E. c  e.  ( Fin  i^i  ~P A ) c `' [ C.]  b )
5756expr 613 . . . . . . . . 9  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  d  e.  A )  ->  ( -.  d  e.  b  ->  E. c  e.  ( Fin  i^i  ~P A ) c `' [ C.]  b ) )
5857con1d 124 . . . . . . . 8  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  d  e.  A )  ->  ( -.  E. c  e.  ( Fin  i^i  ~P A ) c `' [ C.]  b  ->  d  e.  b ) )
5924, 58syl5bi 217 . . . . . . 7  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  d  e.  A )  ->  ( A. c  e.  ( Fin  i^i  ~P A )  -.  c `' [ C.]  b  ->  d  e.  b ) )
6059impancom 438 . . . . . 6  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  A. c  e.  ( Fin 
i^i  ~P A )  -.  c `' [ C.]  b
)  ->  ( d  e.  A  ->  d  e.  b ) )
6160ssrdv 3447 . . . . 5  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  A. c  e.  ( Fin 
i^i  ~P A )  -.  c `' [ C.]  b
)  ->  A  C_  b
)
62 ssfi 7774 . . . . 5  |-  ( ( b  e.  Fin  /\  A  C_  b )  ->  A  e.  Fin )
6323, 61, 62syl2anc 659 . . . 4  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  A. c  e.  ( Fin 
i^i  ~P A )  -.  c `' [ C.]  b
)  ->  A  e.  Fin )
6463rexlimiva 2891 . . 3  |-  ( E. b  e.  ( Fin 
i^i  ~P A ) A. c  e.  ( Fin  i^i 
~P A )  -.  c `' [ C.]  b  ->  A  e.  Fin )
6520, 64syl6 31 . 2  |-  ( A  e.  V  ->  ( `' [ C.]  Fr  ~P A  ->  A  e.  Fin )
)
667, 65impbid2 204 1  |-  ( A  e.  V  ->  ( A  e.  Fin  <->  `' [ C.]  Fr  ~P A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1405    e. wcel 1842    =/= wne 2598   A.wral 2753   E.wrex 2754   _Vcvv 3058    u. cun 3411    i^i cin 3412    C_ wss 3413    C. wpss 3414   (/)c0 3737   ~Pcpw 3954   {csn 3971   class class class wbr 4394    Po wpo 4741    Fr wfr 4778   `'ccnv 4821   [ C.] crpss 6560   Fincfn 7553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-reu 2760  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-pss 3429  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-tp 3976  df-op 3978  df-uni 4191  df-int 4227  df-iun 4272  df-br 4395  df-opab 4453  df-mpt 4454  df-tr 4489  df-eprel 4733  df-id 4737  df-po 4743  df-so 4744  df-fr 4781  df-we 4783  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-pred 5366  df-ord 5412  df-on 5413  df-lim 5414  df-suc 5415  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575  df-fv 5576  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-rpss 6561  df-om 6683  df-1st 6783  df-2nd 6784  df-wrecs 7012  df-recs 7074  df-rdg 7112  df-1o 7166  df-2o 7167  df-oadd 7170  df-er 7347  df-map 7458  df-en 7554  df-dom 7555  df-sdom 7556  df-fin 7557
This theorem is referenced by:  isfin1-4  8798  fin12  8824
  Copyright terms: Public domain W3C validator