Theorem powerfin ≪ | index | src | ≫ 

theorem powerfin (A: set): $ finite A -> finite (Power A) $;
StepHypRefExpression
1 dffin2 
finite A <-> E. n A C_ upto n
2 lteq2 
x = suc (upto n) -> (a < x <-> a < suc (upto n))
3 2 imeq2d 
x = suc (upto n) -> (a e. Power A -> a < x <-> a e. Power A -> a < suc (upto n))
4 3 aleqd 
x = suc (upto n) -> (A. a (a e. Power A -> a < x) <-> A. a (a e. Power A -> a < suc (upto n)))
5 4 iexe 
A. a (a e. Power A -> a < suc (upto n)) -> E. x A. a (a e. Power A -> a < x)
6 5 conv finite 
A. a (a e. Power A -> a < suc (upto n)) -> finite (Power A)
7 elPower 
a e. Power A <-> a C_ A
8 leltsuc 
a <= upto n <-> a < suc (upto n)
9 ssle 
a C_ upto n -> a <= upto n
10 8, 9 sylib 
a C_ upto n -> a < suc (upto n)
11 sstr 
a C_ A -> A C_ upto n -> a C_ upto n
12 10, 11 syl6 
a C_ A -> A C_ upto n -> a < suc (upto n)
13 12 com12 
A C_ upto n -> a C_ A -> a < suc (upto n)
14 7, 13 syl5bi 
A C_ upto n -> a e. Power A -> a < suc (upto n)
15 14 iald 
A C_ upto n -> A. a (a e. Power A -> a < suc (upto n))
16 6, 15 syl 
A C_ upto n -> finite (Power A)
17 16 eex 
E. n A C_ upto n -> finite (Power A)
18 1, 17 sylbi 
finite A -> finite (Power A)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)