Metamath Proof Explorer


Theorem cnvfiALT

Description: Shorter proof of cnvfi using ax-pow . (Contributed by Mario Carneiro, 28-Dec-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cnvfiALT
|- ( A e. Fin -> `' A e. Fin )

Proof

Step Hyp Ref Expression
1 cnvcnvss
 |-  `' `' A C_ A
2 ssfi
 |-  ( ( A e. Fin /\ `' `' A C_ A ) -> `' `' A e. Fin )
3 1 2 mpan2
 |-  ( A e. Fin -> `' `' A e. Fin )
4 relcnv
 |-  Rel `' A
5 cnvexg
 |-  ( A e. Fin -> `' A e. _V )
6 cnven
 |-  ( ( Rel `' A /\ `' A e. _V ) -> `' A ~~ `' `' A )
7 4 5 6 sylancr
 |-  ( A e. Fin -> `' A ~~ `' `' A )
8 enfii
 |-  ( ( `' `' A e. Fin /\ `' A ~~ `' `' A ) -> `' A e. Fin )
9 3 7 8 syl2anc
 |-  ( A e. Fin -> `' A e. Fin )