Metamath Proof Explorer


Theorem imafiALT

Description: Shorter proof of imafi using ax-pow . (Contributed by Stefan O'Rear, 22-Feb-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion imafiALT
|- ( ( Fun F /\ X e. Fin ) -> ( F " X ) e. Fin )

Proof

Step Hyp Ref Expression
1 imadmres
 |-  ( F " dom ( F |` X ) ) = ( F " X )
2 simpr
 |-  ( ( Fun F /\ X e. Fin ) -> X e. Fin )
3 dmres
 |-  dom ( F |` X ) = ( X i^i dom F )
4 inss1
 |-  ( X i^i dom F ) C_ X
5 3 4 eqsstri
 |-  dom ( F |` X ) C_ X
6 ssfi
 |-  ( ( X e. Fin /\ dom ( F |` X ) C_ X ) -> dom ( F |` X ) e. Fin )
7 2 5 6 sylancl
 |-  ( ( Fun F /\ X e. Fin ) -> dom ( F |` X ) e. Fin )
8 resss
 |-  ( F |` X ) C_ F
9 dmss
 |-  ( ( F |` X ) C_ F -> dom ( F |` X ) C_ dom F )
10 8 9 mp1i
 |-  ( ( Fun F /\ X e. Fin ) -> dom ( F |` X ) C_ dom F )
11 fores
 |-  ( ( Fun F /\ dom ( F |` X ) C_ dom F ) -> ( F |` dom ( F |` X ) ) : dom ( F |` X ) -onto-> ( F " dom ( F |` X ) ) )
12 10 11 syldan
 |-  ( ( Fun F /\ X e. Fin ) -> ( F |` dom ( F |` X ) ) : dom ( F |` X ) -onto-> ( F " dom ( F |` X ) ) )
13 fofi
 |-  ( ( dom ( F |` X ) e. Fin /\ ( F |` dom ( F |` X ) ) : dom ( F |` X ) -onto-> ( F " dom ( F |` X ) ) ) -> ( F " dom ( F |` X ) ) e. Fin )
14 7 12 13 syl2anc
 |-  ( ( Fun F /\ X e. Fin ) -> ( F " dom ( F |` X ) ) e. Fin )
15 1 14 eqeltrrid
 |-  ( ( Fun F /\ X e. Fin ) -> ( F " X ) e. Fin )