Step |
Hyp |
Ref |
Expression |
1 |
|
1nn |
|- 1 e. NN |
2 |
|
simpr |
|- ( ( A e. ( ~P NN i^i Fin ) /\ A = (/) ) -> A = (/) ) |
3 |
|
0ss |
|- (/) C_ ( 1 ... 1 ) |
4 |
2 3
|
eqsstrdi |
|- ( ( A e. ( ~P NN i^i Fin ) /\ A = (/) ) -> A C_ ( 1 ... 1 ) ) |
5 |
|
oveq2 |
|- ( n = 1 -> ( 1 ... n ) = ( 1 ... 1 ) ) |
6 |
5
|
sseq2d |
|- ( n = 1 -> ( A C_ ( 1 ... n ) <-> A C_ ( 1 ... 1 ) ) ) |
7 |
6
|
rspcev |
|- ( ( 1 e. NN /\ A C_ ( 1 ... 1 ) ) -> E. n e. NN A C_ ( 1 ... n ) ) |
8 |
1 4 7
|
sylancr |
|- ( ( A e. ( ~P NN i^i Fin ) /\ A = (/) ) -> E. n e. NN A C_ ( 1 ... n ) ) |
9 |
|
elin |
|- ( A e. ( ~P NN i^i Fin ) <-> ( A e. ~P NN /\ A e. Fin ) ) |
10 |
9
|
simplbi |
|- ( A e. ( ~P NN i^i Fin ) -> A e. ~P NN ) |
11 |
10
|
adantr |
|- ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> A e. ~P NN ) |
12 |
11
|
elpwid |
|- ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> A C_ NN ) |
13 |
|
nnssre |
|- NN C_ RR |
14 |
|
ltso |
|- < Or RR |
15 |
|
soss |
|- ( NN C_ RR -> ( < Or RR -> < Or NN ) ) |
16 |
13 14 15
|
mp2 |
|- < Or NN |
17 |
16
|
a1i |
|- ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> < Or NN ) |
18 |
9
|
simprbi |
|- ( A e. ( ~P NN i^i Fin ) -> A e. Fin ) |
19 |
18
|
adantr |
|- ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> A e. Fin ) |
20 |
|
simpr |
|- ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> A =/= (/) ) |
21 |
|
fisupcl |
|- ( ( < Or NN /\ ( A e. Fin /\ A =/= (/) /\ A C_ NN ) ) -> sup ( A , NN , < ) e. A ) |
22 |
17 19 20 12 21
|
syl13anc |
|- ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> sup ( A , NN , < ) e. A ) |
23 |
12 22
|
sseldd |
|- ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> sup ( A , NN , < ) e. NN ) |
24 |
12
|
sselda |
|- ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> x e. NN ) |
25 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
26 |
24 25
|
eleqtrdi |
|- ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> x e. ( ZZ>= ` 1 ) ) |
27 |
24
|
nnzd |
|- ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> x e. ZZ ) |
28 |
12
|
adantr |
|- ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> A C_ NN ) |
29 |
22
|
adantr |
|- ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> sup ( A , NN , < ) e. A ) |
30 |
28 29
|
sseldd |
|- ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> sup ( A , NN , < ) e. NN ) |
31 |
30
|
nnzd |
|- ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> sup ( A , NN , < ) e. ZZ ) |
32 |
|
fisup2g |
|- ( ( < Or NN /\ ( A e. Fin /\ A =/= (/) /\ A C_ NN ) ) -> E. x e. A ( A. y e. A -. x < y /\ A. y e. NN ( y < x -> E. z e. A y < z ) ) ) |
33 |
17 19 20 12 32
|
syl13anc |
|- ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> E. x e. A ( A. y e. A -. x < y /\ A. y e. NN ( y < x -> E. z e. A y < z ) ) ) |
34 |
|
ssrexv |
|- ( A C_ NN -> ( E. x e. A ( A. y e. A -. x < y /\ A. y e. NN ( y < x -> E. z e. A y < z ) ) -> E. x e. NN ( A. y e. A -. x < y /\ A. y e. NN ( y < x -> E. z e. A y < z ) ) ) ) |
35 |
12 33 34
|
sylc |
|- ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> E. x e. NN ( A. y e. A -. x < y /\ A. y e. NN ( y < x -> E. z e. A y < z ) ) ) |
36 |
17 35
|
supub |
|- ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> ( x e. A -> -. sup ( A , NN , < ) < x ) ) |
37 |
36
|
imp |
|- ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> -. sup ( A , NN , < ) < x ) |
38 |
24
|
nnred |
|- ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> x e. RR ) |
39 |
30
|
nnred |
|- ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> sup ( A , NN , < ) e. RR ) |
40 |
38 39
|
lenltd |
|- ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> ( x <_ sup ( A , NN , < ) <-> -. sup ( A , NN , < ) < x ) ) |
41 |
37 40
|
mpbird |
|- ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> x <_ sup ( A , NN , < ) ) |
42 |
|
eluz2 |
|- ( sup ( A , NN , < ) e. ( ZZ>= ` x ) <-> ( x e. ZZ /\ sup ( A , NN , < ) e. ZZ /\ x <_ sup ( A , NN , < ) ) ) |
43 |
27 31 41 42
|
syl3anbrc |
|- ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> sup ( A , NN , < ) e. ( ZZ>= ` x ) ) |
44 |
|
eluzfz |
|- ( ( x e. ( ZZ>= ` 1 ) /\ sup ( A , NN , < ) e. ( ZZ>= ` x ) ) -> x e. ( 1 ... sup ( A , NN , < ) ) ) |
45 |
26 43 44
|
syl2anc |
|- ( ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) /\ x e. A ) -> x e. ( 1 ... sup ( A , NN , < ) ) ) |
46 |
45
|
ex |
|- ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> ( x e. A -> x e. ( 1 ... sup ( A , NN , < ) ) ) ) |
47 |
46
|
ssrdv |
|- ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> A C_ ( 1 ... sup ( A , NN , < ) ) ) |
48 |
|
oveq2 |
|- ( n = sup ( A , NN , < ) -> ( 1 ... n ) = ( 1 ... sup ( A , NN , < ) ) ) |
49 |
48
|
sseq2d |
|- ( n = sup ( A , NN , < ) -> ( A C_ ( 1 ... n ) <-> A C_ ( 1 ... sup ( A , NN , < ) ) ) ) |
50 |
49
|
rspcev |
|- ( ( sup ( A , NN , < ) e. NN /\ A C_ ( 1 ... sup ( A , NN , < ) ) ) -> E. n e. NN A C_ ( 1 ... n ) ) |
51 |
23 47 50
|
syl2anc |
|- ( ( A e. ( ~P NN i^i Fin ) /\ A =/= (/) ) -> E. n e. NN A C_ ( 1 ... n ) ) |
52 |
8 51
|
pm2.61dane |
|- ( A e. ( ~P NN i^i Fin ) -> E. n e. NN A C_ ( 1 ... n ) ) |