Theorem sssize ≪ | index | src | ≫ 

theorem sssize (A: set): $ finite A <-> A C_ upto (size A) $;
StepHypRefExpression
1 bitr 
(finite A <-> E. n A C_ upto n) -> (E. n A C_ upto n <-> A C_ upto (size A)) -> (finite A <-> A C_ upto (size A))
2 dffin2 
finite A <-> E. n A C_ upto n
3 1, 2 ax_mp 
(E. n A C_ upto n <-> A C_ upto (size A)) -> (finite A <-> A C_ upto (size A))
4 uptoeq 
k = n -> upto k = upto n
5 4 nseqd 
k = n -> upto k == upto n
6 5 sseq2d 
k = n -> (A C_ upto k <-> A C_ upto n)
7 6 elabe 
n e. {k | A C_ upto k} <-> A C_ upto n
8 uptoeq 
k = size A -> upto k = upto (size A)
9 8 nseqd 
k = size A -> upto k == upto (size A)
10 9 sseq2d 
k = size A -> (A C_ upto k <-> A C_ upto (size A))
11 10 elabe 
size A e. {k | A C_ upto k} <-> A C_ upto (size A)
12 leastel 
n e. {k | A C_ upto k} -> least {k | A C_ upto k} e. {k | A C_ upto k}
13 12 conv size 
n e. {k | A C_ upto k} -> size A e. {k | A C_ upto k}
14 11, 13 sylib 
n e. {k | A C_ upto k} -> A C_ upto (size A)
15 7, 14 sylbir 
A C_ upto n -> A C_ upto (size A)
16 15 eex 
E. n A C_ upto n -> A C_ upto (size A)
17 uptoeq 
n = size A -> upto n = upto (size A)
18 17 nseqd 
n = size A -> upto n == upto (size A)
19 18 sseq2d 
n = size A -> (A C_ upto n <-> A C_ upto (size A))
20 19 iexe 
A C_ upto (size A) -> E. n A C_ upto n
21 16, 20 ibii 
E. n A C_ upto n <-> A C_ upto (size A)
22 3, 21 ax_mp 
finite A <-> A C_ upto (size 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)