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

Theorem isfin1-3 8821
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 6580 . . . 4  |- [ C.]  Po  ~P A
2 cnvpo 5377 . . . 4  |-  ( [ C.]  Po  ~P A  <->  `' [ C.]  Po  ~P A )
31, 2mpbi 212 . . 3  |-  `' [ C.]  Po  ~P A
4 pwfi 7874 . . . 4  |-  ( A  e.  Fin  <->  ~P A  e.  Fin )
54biimpi 198 . . 3  |-  ( A  e.  Fin  ->  ~P A  e.  Fin )
6 frfi 7821 . . 3  |-  ( ( `' [ C.]  Po  ~P A  /\  ~P A  e.  Fin )  ->  `' [ C.]  Fr  ~P A )
73, 5, 6sylancr 670 . 2  |-  ( A  e.  Fin  ->  `' [ C.] 
Fr  ~P A )
8 inss2 3655 . . . . . 6  |-  ( Fin 
i^i  ~P A )  C_  ~P A
9 pwexg 4590 . . . . . 6  |-  ( A  e.  V  ->  ~P A  e.  _V )
10 ssexg 4552 . . . . . 6  |-  ( ( ( Fin  i^i  ~P A )  C_  ~P A  /\  ~P A  e. 
_V )  ->  ( Fin  i^i  ~P A )  e.  _V )
118, 9, 10sylancr 670 . . . . 5  |-  ( A  e.  V  ->  ( Fin  i^i  ~P A )  e.  _V )
12 0fin 7804 . . . . . . . 8  |-  (/)  e.  Fin
13 0elpw 4575 . . . . . . . 8  |-  (/)  e.  ~P A
14 elin 3619 . . . . . . . 8  |-  ( (/)  e.  ( Fin  i^i  ~P A )  <->  ( (/)  e.  Fin  /\  (/)  e.  ~P A ) )
1512, 13, 14mpbir2an 932 . . . . . . 7  |-  (/)  e.  ( Fin  i^i  ~P A
)
1615ne0ii 3740 . . . . . 6  |-  ( Fin 
i^i  ~P A )  =/=  (/)
17 fri 4799 . . . . . 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 692 . . . . 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 474 . . . 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 436 . . 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 3654 . . . . . 6  |-  ( Fin 
i^i  ~P A )  C_  Fin
22 simpl 459 . . . . . 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 3432 . . . . 5  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  A. c  e.  ( Fin 
i^i  ~P A )  -.  c `' [ C.]  b
)  ->  b  e.  Fin )
24 ralnex 2836 . . . . . . . 8  |-  ( A. c  e.  ( Fin  i^i 
~P A )  -.  c `' [ C.]  b  <->  -. 
E. c  e.  ( Fin  i^i  ~P A
) c `' [ C.]  b
)
2521sseli 3430 . . . . . . . . . . . . . 14  |-  ( b  e.  ( Fin  i^i  ~P A )  ->  b  e.  Fin )
2625adantr 467 . . . . . . . . . . . . 13  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  ( d  e.  A  /\  -.  d  e.  b ) )  ->  b  e.  Fin )
27 snfi 7655 . . . . . . . . . . . . 13  |-  { d }  e.  Fin
28 unfi 7843 . . . . . . . . . . . . 13  |-  ( ( b  e.  Fin  /\  { d }  e.  Fin )  ->  ( b  u. 
{ d } )  e.  Fin )
2926, 27, 28sylancl 669 . . . . . . . . . . . 12  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  ( d  e.  A  /\  -.  d  e.  b ) )  ->  (
b  u.  { d } )  e.  Fin )
30 elin 3619 . . . . . . . . . . . . . . . . 17  |-  ( b  e.  ( Fin  i^i  ~P A )  <->  ( b  e.  Fin  /\  b  e. 
~P A ) )
3130simprbi 466 . . . . . . . . . . . . . . . 16  |-  ( b  e.  ( Fin  i^i  ~P A )  ->  b  e.  ~P A )
3231elpwid 3963 . . . . . . . . . . . . . . 15  |-  ( b  e.  ( Fin  i^i  ~P A )  ->  b  C_  A )
3332adantr 467 . . . . . . . . . . . . . 14  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  ( d  e.  A  /\  -.  d  e.  b ) )  ->  b  C_  A )
34 snssi 4119 . . . . . . . . . . . . . . 15  |-  ( d  e.  A  ->  { d }  C_  A )
3534ad2antrl 735 . . . . . . . . . . . . . 14  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  ( d  e.  A  /\  -.  d  e.  b ) )  ->  { d }  C_  A )
3633, 35unssd 3612 . . . . . . . . . . . . 13  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  ( d  e.  A  /\  -.  d  e.  b ) )  ->  (
b  u.  { d } )  C_  A
)
37 vex 3050 . . . . . . . . . . . . . . 15  |-  b  e. 
_V
38 snex 4644 . . . . . . . . . . . . . . 15  |-  { d }  e.  _V
3937, 38unex 6594 . . . . . . . . . . . . . 14  |-  ( b  u.  { d } )  e.  _V
4039elpw 3959 . . . . . . . . . . . . 13  |-  ( ( b  u.  { d } )  e.  ~P A 
<->  ( b  u.  {
d } )  C_  A )
4136, 40sylibr 216 . . . . . . . . . . . 12  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  ( d  e.  A  /\  -.  d  e.  b ) )  ->  (
b  u.  { d } )  e.  ~P A )
4229, 41elind 3620 . . . . . . . . . . 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 4034 . . . . . . . . . . . . . . 15  |-  ( ( b  i^i  { d } )  =  (/)  <->  -.  d  e.  b )
4443biimpri 210 . . . . . . . . . . . . . 14  |-  ( -.  d  e.  b  -> 
( b  i^i  {
d } )  =  (/) )
45 vex 3050 . . . . . . . . . . . . . . 15  |-  d  e. 
_V
4645snnz 4093 . . . . . . . . . . . . . 14  |-  { d }  =/=  (/)
47 disjpss 3817 . . . . . . . . . . . . . 14  |-  ( ( ( b  i^i  {
d } )  =  (/)  /\  { d }  =/=  (/) )  ->  b  C.  ( b  u.  {
d } ) )
4844, 46, 47sylancl 669 . . . . . . . . . . . . 13  |-  ( -.  d  e.  b  -> 
b  C.  ( b  u.  { d } ) )
4948ad2antll 736 . . . . . . . . . . . 12  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  ( d  e.  A  /\  -.  d  e.  b ) )  ->  b  C.  ( b  u.  {
d } ) )
5039, 37brcnv 5020 . . . . . . . . . . . . 13  |-  ( ( b  u.  { d } ) `' [ C.]  b  <->  b [ C.]  ( b  u.  {
d } ) )
5139brrpss 6579 . . . . . . . . . . . . 13  |-  ( b [ C.]  ( b  u.  {
d } )  <->  b  C.  (
b  u.  { d } ) )
5250, 51bitri 253 . . . . . . . . . . . 12  |-  ( ( b  u.  { d } ) `' [ C.]  b  <->  b 
C.  ( b  u. 
{ d } ) )
5349, 52sylibr 216 . . . . . . . . . . 11  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  ( d  e.  A  /\  -.  d  e.  b ) )  ->  (
b  u.  { d } ) `' [ C.]  b
)
54 breq1 4408 . . . . . . . . . . . 12  |-  ( c  =  ( b  u. 
{ d } )  ->  ( c `' [ C.]  b  <->  ( b  u. 
{ d } ) `' [ C.]  b ) )
5554rspcev 3152 . . . . . . . . . . 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 667 . . . . . . . . . 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 620 . . . . . . . . 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 128 . . . . . . . 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 221 . . . . . . 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 442 . . . . . 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 3440 . . . . 5  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  A. c  e.  ( Fin 
i^i  ~P A )  -.  c `' [ C.]  b
)  ->  A  C_  b
)
62 ssfi 7797 . . . . 5  |-  ( ( b  e.  Fin  /\  A  C_  b )  ->  A  e.  Fin )
6323, 61, 62syl2anc 667 . . . 4  |-  ( ( b  e.  ( Fin 
i^i  ~P A )  /\  A. c  e.  ( Fin 
i^i  ~P A )  -.  c `' [ C.]  b
)  ->  A  e.  Fin )
6463rexlimiva 2877 . . 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 34 . 2  |-  ( A  e.  V  ->  ( `' [ C.]  Fr  ~P A  ->  A  e.  Fin )
)
667, 65impbid2 208 1  |-  ( A  e.  V  ->  ( A  e.  Fin  <->  `' [ C.]  Fr  ~P A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1446    e. wcel 1889    =/= wne 2624   A.wral 2739   E.wrex 2740   _Vcvv 3047    u. cun 3404    i^i cin 3405    C_ wss 3406    C. wpss 3407   (/)c0 3733   ~Pcpw 3953   {csn 3970   class class class wbr 4405    Po wpo 4756    Fr wfr 4793   `'ccnv 4836   [ C.] crpss 6575   Fincfn 7574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-reu 2746  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-int 4238  df-iun 4283  df-br 4406  df-opab 4465  df-mpt 4466  df-tr 4501  df-eprel 4748  df-id 4752  df-po 4758  df-so 4759  df-fr 4796  df-we 4798  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-pred 5383  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-rpss 6576  df-om 6698  df-1st 6798  df-2nd 6799  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-1o 7187  df-2o 7188  df-oadd 7191  df-er 7368  df-map 7479  df-en 7575  df-dom 7576  df-sdom 7577  df-fin 7578
This theorem is referenced by:  isfin1-4  8822  fin12  8848
  Copyright terms: Public domain W3C validator