Metamath Proof Explorer

Theorem pwfilemOLD

Description: Obsolete version of pwfilem as of 7-Sep-2024. (Contributed by NM, 26-Mar-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis pwfilemOLD.1 
|- F = ( c e. ~P b |-> ( c u. { x } ) )
Assertion pwfilemOLD 
|- ( ~P b e. Fin -> ~P ( b u. { x } ) e. Fin )

Proof

Step Hyp Ref Expression
1 pwfilemOLD.1 
 |-  F = ( c e. ~P b |-> ( c u. { x } ) )
2 pwundif 
 |-  ~P ( b u. { x } ) = ( ( ~P ( b u. { x } ) \ ~P b ) u. ~P b )
3 vex 
 |-  c e. _V
4 snex 
 |-  { x } e. _V
5 3 4 unex 
 |-  ( c u. { x } ) e. _V
6 5 1 fnmpti 
 |-  F Fn ~P b
7 dffn4 
 |-  ( F Fn ~P b <-> F : ~P b -onto-> ran F )
8 6 7 mpbi 
 |-  F : ~P b -onto-> ran F
9 fodomfi 
 |-  ( ( ~P b e. Fin /\ F : ~P b -onto-> ran F ) -> ran F ~<_ ~P b )
10 8 9 mpan2 
 |-  ( ~P b e. Fin -> ran F ~<_ ~P b )
11 domfi 
 |-  ( ( ~P b e. Fin /\ ran F ~<_ ~P b ) -> ran F e. Fin )
12 10 11 mpdan 
 |-  ( ~P b e. Fin -> ran F e. Fin )
13 eldifi 
 |-  ( d e. ( ~P ( b u. { x } ) \ ~P b ) -> d e. ~P ( b u. { x } ) )
14 4 elpwun 
 |-  ( d e. ~P ( b u. { x } ) <-> ( d \ { x } ) e. ~P b )
15 13 14 sylib 
 |-  ( d e. ( ~P ( b u. { x } ) \ ~P b ) -> ( d \ { x } ) e. ~P b )
16 undif1 
 |-  ( ( d \ { x } ) u. { x } ) = ( d u. { x } )
17 elpwunsn 
 |-  ( d e. ( ~P ( b u. { x } ) \ ~P b ) -> x e. d )
18 17 snssd 
 |-  ( d e. ( ~P ( b u. { x } ) \ ~P b ) -> { x } C_ d )
19 ssequn2 
 |-  ( { x } C_ d <-> ( d u. { x } ) = d )
20 18 19 sylib 
 |-  ( d e. ( ~P ( b u. { x } ) \ ~P b ) -> ( d u. { x } ) = d )
21 16 20 eqtr2id 
 |-  ( d e. ( ~P ( b u. { x } ) \ ~P b ) -> d = ( ( d \ { x } ) u. { x } ) )
22 uneq1 
 |-  ( c = ( d \ { x } ) -> ( c u. { x } ) = ( ( d \ { x } ) u. { x } ) )
23 22 rspceeqv 
 |-  ( ( ( d \ { x } ) e. ~P b /\ d = ( ( d \ { x } ) u. { x } ) ) -> E. c e. ~P b d = ( c u. { x } ) )
24 15 21 23 syl2anc 
 |-  ( d e. ( ~P ( b u. { x } ) \ ~P b ) -> E. c e. ~P b d = ( c u. { x } ) )
25 1 5 elrnmpti 
 |-  ( d e. ran F <-> E. c e. ~P b d = ( c u. { x } ) )
26 24 25 sylibr 
 |-  ( d e. ( ~P ( b u. { x } ) \ ~P b ) -> d e. ran F )
27 26 ssriv 
 |-  ( ~P ( b u. { x } ) \ ~P b ) C_ ran F
28 ssdomg 
 |-  ( ran F e. Fin -> ( ( ~P ( b u. { x } ) \ ~P b ) C_ ran F -> ( ~P ( b u. { x } ) \ ~P b ) ~<_ ran F ) )
29 12 27 28 mpisyl 
 |-  ( ~P b e. Fin -> ( ~P ( b u. { x } ) \ ~P b ) ~<_ ran F )
30 domfi 
 |-  ( ( ran F e. Fin /\ ( ~P ( b u. { x } ) \ ~P b ) ~<_ ran F ) -> ( ~P ( b u. { x } ) \ ~P b ) e. Fin )
31 12 29 30 syl2anc 
 |-  ( ~P b e. Fin -> ( ~P ( b u. { x } ) \ ~P b ) e. Fin )
32 unfi 
 |-  ( ( ( ~P ( b u. { x } ) \ ~P b ) e. Fin /\ ~P b e. Fin ) -> ( ( ~P ( b u. { x } ) \ ~P b ) u. ~P b ) e. Fin )
33 31 32 mpancom 
 |-  ( ~P b e. Fin -> ( ( ~P ( b u. { x } ) \ ~P b ) u. ~P b ) e. Fin )
34 2 33 eqeltrid 
 |-  ( ~P b e. Fin -> ~P ( b u. { x } ) e. Fin )