Metamath Proof Explorer


Theorem ssfiALT

Description: Shorter proof of ssfi using ax-pow . (Contributed by NM, 24-Jun-1998) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ssfiALT A Fin B A B Fin

Proof

Step Hyp Ref Expression
1 isfi A Fin x ω A x
2 bren A x z z : A 1-1 onto x
3 f1ofo z : A 1-1 onto x z : A onto x
4 imassrn z B ran z
5 forn z : A onto x ran z = x
6 4 5 sseqtrid z : A onto x z B x
7 3 6 syl z : A 1-1 onto x z B x
8 ssnnfi x ω z B x z B Fin
9 isfi z B Fin y ω z B y
10 8 9 sylib x ω z B x y ω z B y
11 7 10 sylan2 x ω z : A 1-1 onto x y ω z B y
12 11 adantrr x ω z : A 1-1 onto x B A y ω z B y
13 f1of1 z : A 1-1 onto x z : A 1-1 x
14 f1ores z : A 1-1 x B A z B : B 1-1 onto z B
15 13 14 sylan z : A 1-1 onto x B A z B : B 1-1 onto z B
16 vex z V
17 16 resex z B V
18 f1oeq1 x = z B x : B 1-1 onto z B z B : B 1-1 onto z B
19 17 18 spcev z B : B 1-1 onto z B x x : B 1-1 onto z B
20 bren B z B x x : B 1-1 onto z B
21 19 20 sylibr z B : B 1-1 onto z B B z B
22 entr B z B z B y B y
23 21 22 sylan z B : B 1-1 onto z B z B y B y
24 15 23 sylan z : A 1-1 onto x B A z B y B y
25 24 ex z : A 1-1 onto x B A z B y B y
26 25 reximdv z : A 1-1 onto x B A y ω z B y y ω B y
27 isfi B Fin y ω B y
28 26 27 syl6ibr z : A 1-1 onto x B A y ω z B y B Fin
29 28 adantl x ω z : A 1-1 onto x B A y ω z B y B Fin
30 12 29 mpd x ω z : A 1-1 onto x B A B Fin
31 30 exp32 x ω z : A 1-1 onto x B A B Fin
32 31 exlimdv x ω z z : A 1-1 onto x B A B Fin
33 2 32 syl5bi x ω A x B A B Fin
34 33 rexlimiv x ω A x B A B Fin
35 1 34 sylbi A Fin B A B Fin
36 35 imp A Fin B A B Fin