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 Fin F X Fin

Proof

Step Hyp Ref Expression
1 imadmres F dom F X = F X
2 simpr Fun F X Fin X Fin
3 dmres dom F X = X dom F
4 inss1 X dom F X
5 3 4 eqsstri dom F X X
6 ssfi X Fin dom F X X dom F X Fin
7 2 5 6 sylancl Fun F X Fin dom F X Fin
8 resss F X F
9 dmss F X F dom F X dom F
10 8 9 mp1i Fun F X Fin dom F X dom F
11 fores Fun F dom F X dom F F dom F X : dom F X onto F dom F X
12 10 11 syldan Fun F X Fin F dom F X : dom F X onto F dom F X
13 fofi dom F X Fin F dom F X : dom F X onto F dom F X F dom F X Fin
14 7 12 13 syl2anc Fun F X Fin F dom F X Fin
15 1 14 eqeltrrid Fun F X Fin F X Fin