This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pwfilem

Description: Lemma for pwfi . (Contributed by NM, 26-Mar-2007) Avoid ax-pow . (Revised by BTernaryTau, 7-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 pwfilem.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 1 funmpt2 
 |-  Fun F
4 vex 
 |-  c e. _V
5 vsnex 
 |-  { x } e. _V
6 4 5 unex 
 |-  ( c u. { x } ) e. _V
7 6 1 dmmpti 
 |-  dom F = ~P b
8 7 imaeq2i 
 |-  ( F " dom F ) = ( F " ~P b )
9 imadmrn 
 |-  ( F " dom F ) = ran F
10 8 9 eqtr3i 
 |-  ( F " ~P b ) = ran F
11 imafi 
 |-  ( ( Fun F /\ ~P b e. Fin ) -> ( F " ~P b ) e. Fin )
12 10 11 eqeltrrid 
 |-  ( ( Fun F /\ ~P b e. Fin ) -> ran F e. Fin )
13 3 12 mpan 
 |-  ( ~P b e. Fin -> ran F e. Fin )
14 eldifi 
 |-  ( d e. ( ~P ( b u. { x } ) \ ~P b ) -> d e. ~P ( b u. { x } ) )
15 5 elpwun 
 |-  ( d e. ~P ( b u. { x } ) <-> ( d \ { x } ) e. ~P b )
16 14 15 sylib 
 |-  ( d e. ( ~P ( b u. { x } ) \ ~P b ) -> ( d \ { x } ) e. ~P b )
17 undif1 
 |-  ( ( d \ { x } ) u. { x } ) = ( d u. { x } )
18 elpwunsn 
 |-  ( d e. ( ~P ( b u. { x } ) \ ~P b ) -> x e. d )
19 18 snssd 
 |-  ( d e. ( ~P ( b u. { x } ) \ ~P b ) -> { x } C_ d )
20 ssequn2 
 |-  ( { x } C_ d <-> ( d u. { x } ) = d )
21 19 20 sylib 
 |-  ( d e. ( ~P ( b u. { x } ) \ ~P b ) -> ( d u. { x } ) = d )
22 17 21 eqtr2id 
 |-  ( d e. ( ~P ( b u. { x } ) \ ~P b ) -> d = ( ( d \ { x } ) u. { x } ) )
23 uneq1 
 |-  ( c = ( d \ { x } ) -> ( c u. { x } ) = ( ( d \ { x } ) u. { x } ) )
24 23 rspceeqv 
 |-  ( ( ( d \ { x } ) e. ~P b /\ d = ( ( d \ { x } ) u. { x } ) ) -> E. c e. ~P b d = ( c u. { x } ) )
25 16 22 24 syl2anc 
 |-  ( d e. ( ~P ( b u. { x } ) \ ~P b ) -> E. c e. ~P b d = ( c u. { x } ) )
26 1 25 14 elrnmptd 
 |-  ( 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 ssfi 
 |-  ( ( ran F e. Fin /\ ( ~P ( b u. { x } ) \ ~P b ) C_ ran F ) -> ( ~P ( b u. { x } ) \ ~P b ) e. Fin )
29 13 27 28 sylancl 
 |-  ( ~P b e. Fin -> ( ~P ( b u. { x } ) \ ~P b ) e. Fin )
30 unfi 
 |-  ( ( ( ~P ( b u. { x } ) \ ~P b ) e. Fin /\ ~P b e. Fin ) -> ( ( ~P ( b u. { x } ) \ ~P b ) u. ~P b ) e. Fin )
31 29 30 mpancom 
 |-  ( ~P b e. Fin -> ( ( ~P ( b u. { x } ) \ ~P b ) u. ~P b ) e. Fin )
32 2 31 eqeltrid 
 |-  ( ~P b e. Fin -> ~P ( b u. { x } ) e. Fin )