Step |
Hyp |
Ref |
Expression |
1 |
|
mapfi |
|- ( ( A e. Fin /\ A e. Fin ) -> ( A ^m A ) e. Fin ) |
2 |
|
f1of |
|- ( f : A -1-1-onto-> A -> f : A --> A ) |
3 |
2
|
adantr |
|- ( ( f : A -1-1-onto-> A /\ ph ) -> f : A --> A ) |
4 |
|
elmapg |
|- ( ( A e. Fin /\ A e. Fin ) -> ( f e. ( A ^m A ) <-> f : A --> A ) ) |
5 |
3 4
|
syl5ibr |
|- ( ( A e. Fin /\ A e. Fin ) -> ( ( f : A -1-1-onto-> A /\ ph ) -> f e. ( A ^m A ) ) ) |
6 |
5
|
abssdv |
|- ( ( A e. Fin /\ A e. Fin ) -> { f | ( f : A -1-1-onto-> A /\ ph ) } C_ ( A ^m A ) ) |
7 |
|
ssfi |
|- ( ( ( A ^m A ) e. Fin /\ { f | ( f : A -1-1-onto-> A /\ ph ) } C_ ( A ^m A ) ) -> { f | ( f : A -1-1-onto-> A /\ ph ) } e. Fin ) |
8 |
1 6 7
|
syl2anc |
|- ( ( A e. Fin /\ A e. Fin ) -> { f | ( f : A -1-1-onto-> A /\ ph ) } e. Fin ) |
9 |
8
|
anidms |
|- ( A e. Fin -> { f | ( f : A -1-1-onto-> A /\ ph ) } e. Fin ) |