Metamath Proof Explorer

Theorem fnfi

Description: A version of fnex for finite sets that does not require Replacement. (Contributed by Mario Carneiro, 16-Nov-2014) (Revised by Mario Carneiro, 24-Jun-2015)

Ref Expression
Assertion fnfi 
|- ( ( F Fn A /\ A e. Fin ) -> F e. Fin )

Proof

Step Hyp Ref Expression
1 fnresdm 
 |-  ( F Fn A -> ( F |` A ) = F )
2 1 adantr 
 |-  ( ( F Fn A /\ A e. Fin ) -> ( F |` A ) = F )
3 reseq2 
 |-  ( x = (/) -> ( F |` x ) = ( F |` (/) ) )
4 3 eleq1d 
 |-  ( x = (/) -> ( ( F |` x ) e. Fin <-> ( F |` (/) ) e. Fin ) )
5 4 imbi2d 
 |-  ( x = (/) -> ( ( ( F Fn A /\ A e. Fin ) -> ( F |` x ) e. Fin ) <-> ( ( F Fn A /\ A e. Fin ) -> ( F |` (/) ) e. Fin ) ) )
6 reseq2 
 |-  ( x = y -> ( F |` x ) = ( F |` y ) )
7 6 eleq1d 
 |-  ( x = y -> ( ( F |` x ) e. Fin <-> ( F |` y ) e. Fin ) )
8 7 imbi2d 
 |-  ( x = y -> ( ( ( F Fn A /\ A e. Fin ) -> ( F |` x ) e. Fin ) <-> ( ( F Fn A /\ A e. Fin ) -> ( F |` y ) e. Fin ) ) )
9 reseq2 
 |-  ( x = ( y u. { z } ) -> ( F |` x ) = ( F |` ( y u. { z } ) ) )
10 9 eleq1d 
 |-  ( x = ( y u. { z } ) -> ( ( F |` x ) e. Fin <-> ( F |` ( y u. { z } ) ) e. Fin ) )
11 10 imbi2d 
 |-  ( x = ( y u. { z } ) -> ( ( ( F Fn A /\ A e. Fin ) -> ( F |` x ) e. Fin ) <-> ( ( F Fn A /\ A e. Fin ) -> ( F |` ( y u. { z } ) ) e. Fin ) ) )
12 reseq2 
 |-  ( x = A -> ( F |` x ) = ( F |` A ) )
13 12 eleq1d 
 |-  ( x = A -> ( ( F |` x ) e. Fin <-> ( F |` A ) e. Fin ) )
14 13 imbi2d 
 |-  ( x = A -> ( ( ( F Fn A /\ A e. Fin ) -> ( F |` x ) e. Fin ) <-> ( ( F Fn A /\ A e. Fin ) -> ( F |` A ) e. Fin ) ) )
15 res0 
 |-  ( F |` (/) ) = (/)
16 0fin 
 |-  (/) e. Fin
17 15 16 eqeltri 
 |-  ( F |` (/) ) e. Fin
18 17 a1i 
 |-  ( ( F Fn A /\ A e. Fin ) -> ( F |` (/) ) e. Fin )
19 resundi 
 |-  ( F |` ( y u. { z } ) ) = ( ( F |` y ) u. ( F |` { z } ) )
20 snfi 
 |-  { <. z , ( F ` z ) >. } e. Fin
21 fnfun 
 |-  ( F Fn A -> Fun F )
22 funressn 
 |-  ( Fun F -> ( F |` { z } ) C_ { <. z , ( F ` z ) >. } )
23 21 22 syl 
 |-  ( F Fn A -> ( F |` { z } ) C_ { <. z , ( F ` z ) >. } )
24 23 adantr 
 |-  ( ( F Fn A /\ A e. Fin ) -> ( F |` { z } ) C_ { <. z , ( F ` z ) >. } )
25 ssfi 
 |-  ( ( { <. z , ( F ` z ) >. } e. Fin /\ ( F |` { z } ) C_ { <. z , ( F ` z ) >. } ) -> ( F |` { z } ) e. Fin )
26 20 24 25 sylancr 
 |-  ( ( F Fn A /\ A e. Fin ) -> ( F |` { z } ) e. Fin )
27 unfi 
 |-  ( ( ( F |` y ) e. Fin /\ ( F |` { z } ) e. Fin ) -> ( ( F |` y ) u. ( F |` { z } ) ) e. Fin )
28 26 27 sylan2 
 |-  ( ( ( F |` y ) e. Fin /\ ( F Fn A /\ A e. Fin ) ) -> ( ( F |` y ) u. ( F |` { z } ) ) e. Fin )
29 19 28 eqeltrid 
 |-  ( ( ( F |` y ) e. Fin /\ ( F Fn A /\ A e. Fin ) ) -> ( F |` ( y u. { z } ) ) e. Fin )
30 29 expcom 
 |-  ( ( F Fn A /\ A e. Fin ) -> ( ( F |` y ) e. Fin -> ( F |` ( y u. { z } ) ) e. Fin ) )
31 30 a2i 
 |-  ( ( ( F Fn A /\ A e. Fin ) -> ( F |` y ) e. Fin ) -> ( ( F Fn A /\ A e. Fin ) -> ( F |` ( y u. { z } ) ) e. Fin ) )
32 31 a1i 
 |-  ( y e. Fin -> ( ( ( F Fn A /\ A e. Fin ) -> ( F |` y ) e. Fin ) -> ( ( F Fn A /\ A e. Fin ) -> ( F |` ( y u. { z } ) ) e. Fin ) ) )
33 5 8 11 14 18 32 findcard2 
 |-  ( A e. Fin -> ( ( F Fn A /\ A e. Fin ) -> ( F |` A ) e. Fin ) )
34 33 anabsi7 
 |-  ( ( F Fn A /\ A e. Fin ) -> ( F |` A ) e. Fin )
35 2 34 eqeltrrd 
 |-  ( ( F Fn A /\ A e. Fin ) -> F e. Fin )