MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pwfilem Unicode version

Theorem pwfilem 7338
Description: Lemma for pwfi 7339. (Contributed by NM, 26-Mar-2007.)
Hypothesis
Ref Expression
pwfilem.1  |-  F  =  ( c  e.  ~P b  |->  ( c  u. 
{ x } ) )
Assertion
Ref Expression
pwfilem  |-  ( ~P b  e.  Fin  ->  ~P ( b  u.  {
x } )  e. 
Fin )
Distinct variable groups:    b, c    x, c
Allowed substitution hints:    F( x, b, c)

Proof of Theorem pwfilem
Dummy variable  d is distinct from all other variables.
StepHypRef Expression
1 pwundif 4433 . 2  |-  ~P (
b  u.  { x } )  =  ( ( ~P ( b  u.  { x }
)  \  ~P b
)  u.  ~P b
)
2 vex 2904 . . . . . . . . 9  |-  c  e. 
_V
3 snex 4348 . . . . . . . . 9  |-  { x }  e.  _V
42, 3unex 4649 . . . . . . . 8  |-  ( c  u.  { x }
)  e.  _V
5 pwfilem.1 . . . . . . . 8  |-  F  =  ( c  e.  ~P b  |->  ( c  u. 
{ x } ) )
64, 5fnmpti 5515 . . . . . . 7  |-  F  Fn  ~P b
7 dffn4 5601 . . . . . . 7  |-  ( F  Fn  ~P b  <->  F : ~P b -onto-> ran  F )
86, 7mpbi 200 . . . . . 6  |-  F : ~P b -onto-> ran  F
9 fodomfi 7323 . . . . . 6  |-  ( ( ~P b  e.  Fin  /\  F : ~P b -onto-> ran  F )  ->  ran  F  ~<_  ~P b )
108, 9mpan2 653 . . . . 5  |-  ( ~P b  e.  Fin  ->  ran 
F  ~<_  ~P b )
11 domfi 7268 . . . . 5  |-  ( ( ~P b  e.  Fin  /\ 
ran  F  ~<_  ~P b
)  ->  ran  F  e. 
Fin )
1210, 11mpdan 650 . . . 4  |-  ( ~P b  e.  Fin  ->  ran 
F  e.  Fin )
13 eldifi 3414 . . . . . . . . 9  |-  ( d  e.  ( ~P (
b  u.  { x } )  \  ~P b )  ->  d  e.  ~P ( b  u. 
{ x } ) )
143elpwun 4698 . . . . . . . . 9  |-  ( d  e.  ~P ( b  u.  { x }
)  <->  ( d  \  { x } )  e.  ~P b )
1513, 14sylib 189 . . . . . . . 8  |-  ( d  e.  ( ~P (
b  u.  { x } )  \  ~P b )  ->  (
d  \  { x } )  e.  ~P b )
16 undif1 3648 . . . . . . . . 9  |-  ( ( d  \  { x } )  u.  {
x } )  =  ( d  u.  {
x } )
17 elpwunsn 4699 . . . . . . . . . . 11  |-  ( d  e.  ( ~P (
b  u.  { x } )  \  ~P b )  ->  x  e.  d )
1817snssd 3888 . . . . . . . . . 10  |-  ( d  e.  ( ~P (
b  u.  { x } )  \  ~P b )  ->  { x }  C_  d )
19 ssequn2 3465 . . . . . . . . . 10  |-  ( { x }  C_  d  <->  ( d  u.  { x } )  =  d )
2018, 19sylib 189 . . . . . . . . 9  |-  ( d  e.  ( ~P (
b  u.  { x } )  \  ~P b )  ->  (
d  u.  { x } )  =  d )
2116, 20syl5req 2434 . . . . . . . 8  |-  ( d  e.  ( ~P (
b  u.  { x } )  \  ~P b )  ->  d  =  ( ( d 
\  { x }
)  u.  { x } ) )
22 uneq1 3439 . . . . . . . . . 10  |-  ( c  =  ( d  \  { x } )  ->  ( c  u. 
{ x } )  =  ( ( d 
\  { x }
)  u.  { x } ) )
2322eqeq2d 2400 . . . . . . . . 9  |-  ( c  =  ( d  \  { x } )  ->  ( d  =  ( c  u.  {
x } )  <->  d  =  ( ( d  \  { x } )  u.  { x }
) ) )
2423rspcev 2997 . . . . . . . 8  |-  ( ( ( d  \  {
x } )  e. 
~P b  /\  d  =  ( ( d 
\  { x }
)  u.  { x } ) )  ->  E. c  e.  ~P  b d  =  ( c  u.  { x } ) )
2515, 21, 24syl2anc 643 . . . . . . 7  |-  ( d  e.  ( ~P (
b  u.  { x } )  \  ~P b )  ->  E. c  e.  ~P  b d  =  ( c  u.  {
x } ) )
265, 4elrnmpti 5063 . . . . . . 7  |-  ( d  e.  ran  F  <->  E. c  e.  ~P  b d  =  ( c  u.  {
x } ) )
2725, 26sylibr 204 . . . . . 6  |-  ( d  e.  ( ~P (
b  u.  { x } )  \  ~P b )  ->  d  e.  ran  F )
2827ssriv 3297 . . . . 5  |-  ( ~P ( b  u.  {
x } )  \  ~P b )  C_  ran  F
29 ssdomg 7091 . . . . 5  |-  ( ran 
F  e.  Fin  ->  ( ( ~P ( b  u.  { x }
)  \  ~P b
)  C_  ran  F  -> 
( ~P ( b  u.  { x }
)  \  ~P b
)  ~<_  ran  F )
)
3012, 28, 29ee10 1382 . . . 4  |-  ( ~P b  e.  Fin  ->  ( ~P ( b  u. 
{ x } ) 
\  ~P b )  ~<_  ran  F )
31 domfi 7268 . . . 4  |-  ( ( ran  F  e.  Fin  /\  ( ~P ( b  u.  { x }
)  \  ~P b
)  ~<_  ran  F )  ->  ( ~P ( b  u.  { x }
)  \  ~P b
)  e.  Fin )
3212, 30, 31syl2anc 643 . . 3  |-  ( ~P b  e.  Fin  ->  ( ~P ( b  u. 
{ x } ) 
\  ~P b )  e.  Fin )
33 unfi 7312 . . 3  |-  ( ( ( ~P ( b  u.  { x }
)  \  ~P b
)  e.  Fin  /\  ~P b  e.  Fin )  ->  ( ( ~P ( b  u.  {
x } )  \  ~P b )  u.  ~P b )  e.  Fin )
3432, 33mpancom 651 . 2  |-  ( ~P b  e.  Fin  ->  ( ( ~P ( b  u.  { x }
)  \  ~P b
)  u.  ~P b
)  e.  Fin )
351, 34syl5eqel 2473 1  |-  ( ~P b  e.  Fin  ->  ~P ( b  u.  {
x } )  e. 
Fin )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717   E.wrex 2652    \ cdif 3262    u. cun 3263    C_ wss 3265   ~Pcpw 3744   {csn 3759   class class class wbr 4155    e. cmpt 4209   ran crn 4821    Fn wfn 5391   -onto->wfo 5394    ~<_ cdom 7045   Fincfn 7047
This theorem is referenced by:  pwfi  7339
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273  ax-nul 4281  ax-pow 4320  ax-pr 4346  ax-un 4643
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-ral 2656  df-rex 2657  df-reu 2658  df-rab 2660  df-v 2903  df-sbc 3107  df-csb 3197  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-pss 3281  df-nul 3574  df-if 3685  df-pw 3746  df-sn 3765  df-pr 3766  df-tp 3767  df-op 3768  df-uni 3960  df-int 3995  df-iun 4039  df-br 4156  df-opab 4210  df-mpt 4211  df-tr 4246  df-eprel 4437  df-id 4441  df-po 4446  df-so 4447  df-fr 4484  df-we 4486  df-ord 4527  df-on 4528  df-lim 4529  df-suc 4530  df-om 4788  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-rn 4831  df-res 4832  df-ima 4833  df-iota 5360  df-fun 5398  df-fn 5399  df-f 5400  df-f1 5401  df-fo 5402  df-f1o 5403  df-fv 5404  df-ov 6025  df-oprab 6026  df-mpt2 6027  df-recs 6571  df-rdg 6606  df-1o 6662  df-oadd 6666  df-er 6843  df-en 7048  df-dom 7049  df-fin 7051
  Copyright terms: Public domain W3C validator