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 𝐹𝑋 ∈ Fin ) → ( 𝐹𝑋 ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 imadmres ( 𝐹 “ dom ( 𝐹𝑋 ) ) = ( 𝐹𝑋 )
2 simpr ( ( Fun 𝐹𝑋 ∈ Fin ) → 𝑋 ∈ Fin )
3 dmres dom ( 𝐹𝑋 ) = ( 𝑋 ∩ dom 𝐹 )
4 inss1 ( 𝑋 ∩ dom 𝐹 ) ⊆ 𝑋
5 3 4 eqsstri dom ( 𝐹𝑋 ) ⊆ 𝑋
6 ssfi ( ( 𝑋 ∈ Fin ∧ dom ( 𝐹𝑋 ) ⊆ 𝑋 ) → dom ( 𝐹𝑋 ) ∈ Fin )
7 2 5 6 sylancl ( ( Fun 𝐹𝑋 ∈ Fin ) → dom ( 𝐹𝑋 ) ∈ Fin )
8 resss ( 𝐹𝑋 ) ⊆ 𝐹
9 dmss ( ( 𝐹𝑋 ) ⊆ 𝐹 → dom ( 𝐹𝑋 ) ⊆ dom 𝐹 )
10 8 9 mp1i ( ( Fun 𝐹𝑋 ∈ Fin ) → dom ( 𝐹𝑋 ) ⊆ dom 𝐹 )
11 fores ( ( Fun 𝐹 ∧ dom ( 𝐹𝑋 ) ⊆ dom 𝐹 ) → ( 𝐹 ↾ dom ( 𝐹𝑋 ) ) : dom ( 𝐹𝑋 ) –onto→ ( 𝐹 “ dom ( 𝐹𝑋 ) ) )
12 10 11 syldan ( ( Fun 𝐹𝑋 ∈ Fin ) → ( 𝐹 ↾ dom ( 𝐹𝑋 ) ) : dom ( 𝐹𝑋 ) –onto→ ( 𝐹 “ dom ( 𝐹𝑋 ) ) )
13 fofi ( ( dom ( 𝐹𝑋 ) ∈ Fin ∧ ( 𝐹 ↾ dom ( 𝐹𝑋 ) ) : dom ( 𝐹𝑋 ) –onto→ ( 𝐹 “ dom ( 𝐹𝑋 ) ) ) → ( 𝐹 “ dom ( 𝐹𝑋 ) ) ∈ Fin )
14 7 12 13 syl2anc ( ( Fun 𝐹𝑋 ∈ Fin ) → ( 𝐹 “ dom ( 𝐹𝑋 ) ) ∈ Fin )
15 1 14 eqeltrrid ( ( Fun 𝐹𝑋 ∈ Fin ) → ( 𝐹𝑋 ) ∈ Fin )